TY - GEN
T1 - Btor2, BtorMC and Boolector 3.0
AU - Niemetz, Aina
AU - Preiner, Mathias
AU - Wolf, Clifford
AU - Biere, Armin
PY - 2018/8
Y1 - 2018/8
N2 - We describe Btor2, a word-level model checking format for capturing models of hardware and potentially software in a bit-precise manner. This simple, line-based and easy to parse format can be seen as a sorted extension of the word-level format Btor. It uses design principles from the bit-level format Aiger and follows semantics of the SmtLib logics of bit-vectors with arrays. This intermediate format can be used in various verification flows and is perfectly suited to establish a word-level model checking competition. It is supported by our new open source model checker BtorMC, which is built on top of version 3.0 of our SMT solver Boolector. We further provide new word-level benchmarks on which these open source tools are evaluated.
AB - We describe Btor2, a word-level model checking format for capturing models of hardware and potentially software in a bit-precise manner. This simple, line-based and easy to parse format can be seen as a sorted extension of the word-level format Btor. It uses design principles from the bit-level format Aiger and follows semantics of the SmtLib logics of bit-vectors with arrays. This intermediate format can be used in various verification flows and is perfectly suited to establish a word-level model checking competition. It is supported by our new open source model checker BtorMC, which is built on top of version 3.0 of our SMT solver Boolector. We further provide new word-level benchmarks on which these open source tools are evaluated.
UR - https://www.scopus.com/pages/publications/85051107256
U2 - 10.1007/978-3-319-96145-3_32
DO - 10.1007/978-3-319-96145-3_32
M3 - Conference proceedings
VL - vol. 10981
T3 - Lecture Notes in Computer Science (LNCS)
SP - 587
EP - 595
BT - Proc. 30th Intl. Conf. on Computer Aided Verification (CAV'18)
A2 - Weissenbacher, Georg
A2 - Chockler, Hana
PB - Springer
ER -