Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
Computer Aided Verification: Arithmetic Solving in Z3
Beteiligte:
Bjørner, Nikolaj;
Nachmanson, Lev
Erschienen:
Springer Nature Switzerland, 2024
Erschienen in:
Computer Aided Verification (2024), Seite 26-41
Sprache:
Englisch
DOI:
10.1007/978-3-031-65627-9_2
ISBN:
9783031656279;
9783031656262
ISSN:
0302-9743;
1611-3349
Entstehung:
Anmerkungen:
Beschreibung:
AbstractThe theory of arithmetic is integral to many uses of SMT solvers. Z3 has implemented native solvers for arithmetic reasoning since its first release. We present a full re-implementation of Z3’s original arithmetic solver. It is based on substantial experiences from user feedback, engineering and experimentation. While providing a comprehensive overview of the main components we emphasize selected new insights we arrived at while developing and testing the solver.