Detail publikačního výsledku

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic

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

Anglický název

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic

Druh

Stať ve sborníku mimo WoS a Scopus

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.

Anglický 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

Klíčová slova v angličtině

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.

Rok RIV

2025

Vydáno

24.07.2024

Nakladatel

Springer Verlag

Místo

Montreal

Kniha

Proceedings of CAV'24

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"
}