Detail publikace

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic

HABERMEHL Peter, HAVLENA Vojtěch, HEČKO Michal, HOLÍK Lukáš a LENGÁL Ondřej. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. In: Proceedings of CAV'24. Montreal: Springer Verlag, 2024, s. 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
angličtina
Autoři
Habermehl Peter (UPAR7)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Hečko Michal, Ing. (FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
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
Konference
36th International Conference on Computer Aided Verification --- CAV 2024, Montreal, CA
Vydavatel
Springer Verlag
Místo
Montreal, CA
DOI
10.1007/978-3-031-65627-9_3
EID Scopus
2-s2.0-85200742558
BibTeX 
@INPROCEEDINGS{FITPUB13216,
   author = "Peter Habermehl and Vojt\v{e}ch Havlena and Michal He\v{c}ko and Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l",
   title = "Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic",
   pages = "42--67",
   booktitle = "Proceedings of CAV'24",
   journal = "Lecture Notes in Computer Science",
   number = 14681,
   year = 2024,
   location = "Montreal, CA",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-031-65627-9\_3",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13216"
}
Nahoru