Detail publikace

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.; HABERMEHL, P. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. Proceedings of CAV'24. Lecture Notes in Computer Science. Montreal: Springer Verlag, 2024. p. 42-67. ISSN: 0302-9743.
Název česky
Kombinace algebraického a automatového usuzování pro řešení lineární celočíselné aritmetiky
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Havlena Vojtěch, Ing., Ph.D. (UITS)
Hečko Michal, Ing. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Habermehl Peter
Klíčová slova

Presburger arithmetic, linear integer arithmetic, SMT solver, automata-logic connection

Abstrakt

Tento článek ukazuje techniky, jak propojit algebraické usuzování s rozhodovací procedurou pro lineární celočíselnou aritmetiku založenou na automatech pro její citelné zrychlení.

Rok
2024
Strany
42–67
Časopis
Lecture Notes in Computer Science, č. 14681, ISSN 0302-9743
Sborník
Proceedings of CAV'24
Vydavatel
Springer Verlag
Místo
Montreal
DOI
10.1007/978-3-031-65627-9_3
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"
}
Nahoru