A Boolean encoding of arithmetic operations

• Autorzy: Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present algorithms for a Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulae, and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulae.

Słowa kluczowe

EN

Boolean encoding; algorithms; arithmetic operation

PL

kodowanie Boolowskie; algorytmy; działanie matematyczne

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2010
• Tom: Vol. 15
• Strony: 177--190
• Opis fizyczny: Bibliogr. 10 poz.

Twórcy

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, P. Hawkins. The Saturn program analysis system. Technical Report, Stanford University, 2006.
• [2] R. Brummayer, A. Biere. C32SAT: Checking C expressions. In: Proc. CAV`2007, LNCS 4590, pp. 294-297, Springer, Berlin, 2007.
• [3] J.L. Hennessy, D.A. Patterson. Computer Architecture: A Quantitative Approach, 3rd edition. Morgan Kaufmann Publishers, San Francisco, CA, 2003.
• [4] M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, B. Wo¹na, A. Zbrzezny. VerICS 2007 - a model checker for knowledge and real-time. Fund. Informaticae, 85 (1-4), 313-328, 2008.
• [5] A. Niewiadomski, W. Penczek, M. Szreter. A new approach to model checking of UML state machines. Fund. Informaticae, 93 (1-3), 289-303, 2009.
• [6] A. Rataj, B. Wo¹na, A. Zbrzezny. A translator of Java programs to TADDs. Fund. Informaticae, 93 (1-3), 305-324, 2009.
• [7] Y. Xie, A. Aiken. Saturn: A SAT-based tool for bug detection. In: Proc. CAV`2005, LNCS 3576, pp. 139-143. Springer, Berlin, 2005.
• [8] A. Zbrzezny. A boolean encoding of arithmetic operations. Technical Report 999, ICS PAS, 2007.
• [9] A. Zbrzezny, A. Pólrola. SAT-based reachability checking for timed automata with discrete data. Fund. Informaticae, 79 (3 4), 579-593, 2007.
• [10] A. Zbrzezny, B. Wo¹na. Towards verification of Java programs in VerICS. Fund. Informaticae, 85 (1-4), 533-548, 2008.