Journal
COMPUTER AIDED VERIFICATION (CAV 2018), PT I
Volume 10981, Issue -, Pages 587-595Publisher
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-319-96145-3_32
Keywords
-
Funding
- Austrian Science Fund (FWF) under NFN Grant [S11408-N23]
Ask authors/readers for more resources
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 SMT-LIB 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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available