Fast Three-Valued Abstract Bit-Vector Arithmetic

Autoři: doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2022
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Verification, Model Checking, and Abstract Interpretation
Bibliografická citace: ONDERKA, J., RATSCHAN, Stefan. Fast Three-Valued Abstract Bit-Vector Arithmetic. In: FINKBEINER, B., WIES, T., eds. Verification, Model Checking, and Abstract Interpretation. Cham: Springer, 2022, S. 242-262. Lecture Notes on Computer Science, 13182. ISBN 978-3-030-94582-4. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-030-94583-1_12.
DOI: 10.1007/978-3-030-94583-1_12
ID: 556720
Online záznam: Zobrazit online záznam

Abstrakt

Abstraction is one of the most important approaches for reducing the number of states in formal verification. An important abstraction technique is the usage of three-valued logic, extensible to bit-vectors. The best abstract bit-vector results for movement and logical operations can be computed quickly. However, for widely-used arithmetic operations, efficient algorithms for computation of the best possible output have not been known up to now. In this paper, we present new efficient polynomial-time algorithms for abstract addition and multiplication with three-valued bit-vector inputs. These algorithms produce the best possible three-valued bit-vector output and remain fast even with 32-bit inputs. To obtain the algorithms, we devise a novel modular extreme-finding technique via reformulation of the problem using pseudo-Boolean modular inequalities. Using the introduced technique, we construct an algorithm for abstract addition that computes its result in linear time, as well as a worst-case quadratic-time algorithm for abstract multiplication. Finally, we experimentally evaluate the performance of the algorithms, confirming their practical efficiency.