Btor2 , BtorMC and Boolector 3.0
The work
| Authors | Aina Niemetz; Mathias Preiner; Clifford Wolf; Armin Biere |
|---|---|
| Editors | |
| Type | misc |
| Year | 2018 |
| Citekey | niemetz2018btor2 |
Where it appeared
| Published in | Lecture notes in computer science |
|---|---|
| Publisher | Springer Science+Business Media |
| Pages | 587--595 |
Identifiers
| DOI | 10.1007/978-3-319-96145-3_32 |
|---|---|
| OpenAlex | W2884110986 |
Access
| Landing page | https://doi.org/10.1007/978-3-319-96145-3_32 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
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 B tor . 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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 04:06 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{niemetz2018btor2,
title = {Btor2 , BtorMC and Boolector 3.0},
author = {Aina Niemetz and Mathias Preiner and Clifford Wolf and Armin Biere},
year = {2018},
journal = {Lecture notes in computer science},
publisher = {Springer Science+Business Media},
pages = {587--595},
doi = {10.1007/978-3-319-96145-3_32},
}
This record lives at https://refs.drheap.org/niemetz2018btor2/ and will keep doing so.