Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere,
"Btor2, BtorMC and Boolector 3.0"
: Proc. 30th Intl. Conf. on Computer Aided Verification (CAV'18), Serie Lecture Notes in Computer Science (LNCS), Vol. vol. 10981, Springer, Seite(n) 587-595, 8-2018
Btor2, BtorMC and Boolector 3.0
Sprache des Titels:
Proc. 30th Intl. Conf. on Computer Aided Verification (CAV'18)
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 veri?cation ?ows 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.