Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HAVLENA, V. HEČKO, M. HOLÍK, L. LENGÁL, O. HABERMEHL, P.
Originální název
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální abstrakt
We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (nowadays prevalent) algebraic approaches, which work directly with numbers. This combination is enabled by a fine-grained version of the duality between automata and arithmetic formulae. In particular, we employ a construction where states of automaton are obtained as derivatives of arithmetic formulae: then every state corresponds to a formula. Optimizations based on techniques and ideas transferred from the world of algebraic methods are used on thousands of automata states, which dramatically amplifies their effect. The merit of this combination of automata with algebraic methods is demonstrated by our prototype implementation being competitive to and even superior to state-of-the-art SMT solvers.
Klíčová slova
Presburger arithmetic, linear integer arithmetic, SMT solver, automata-logic connection
Autoři
HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.; HABERMEHL, P.
Vydáno
24. 7. 2024
Nakladatel
Springer Verlag
Místo
Montreal
ISSN
0302-9743
Periodikum
Lecture Notes in Computer Science
Číslo
14681
Stát
Spolková republika Německo
Strany od
42
Strany do
67
Strany počet
26
BibTex
@inproceedings{BUT188628, author="Vojtěch {Havlena} and Michal {Hečko} and Lukáš {Holík} and Ondřej {Lengál} and Peter {Habermehl}", title="Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic", booktitle="Proceedings of CAV'24", year="2024", journal="Lecture Notes in Computer Science", number="14681", pages="42--67", publisher="Springer Verlag", address="Montreal", doi="10.1007/978-3-031-65627-9\{_}3", issn="0302-9743" }