Boolector
A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
Documentation
BibTex
Publications
Slides
SMT competitions
People
Download Archive
Third Party Contributions
Publications
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2019.
In Proceedings of the 17th International Workshop on Satisfiability Modulo
Theories (SMT 2019), affiliated with the 22nd International Conference on
Theory and Applications of Satisfiability Testing (SAT 2019), Lisbon, Portugal,
July 7-8, 2019.
[PDF]
[BibTex]
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere.
BTOR2, BtorMC and Boolector 3.0.
In Proceedings of the 30th International Conference on Computer Aided Verification (CAV’18),
Part I,
Lecture Notes in Computer Science,
volume 10981,
pages 587-595,
Springer, 2018.
[PDF]
[DOI]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2018.
Technical Report 18/1,
Stanford University and Johannes Kepler University Linz,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
June 2018.
[PDF]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere.
Propagation based local search for bit-precise reasoning.
In Journal of Formal Methods in System Design,
volume 5 (3), pages 608-636, Springer, 2017.
[Preprint]
[PDF]
[DOI]
[BibTex]
[Artifact]
Aina Niemetz, Mathias Preiner, Armin Biere.
Model-Based API Testing for SMT Solvers.
In Proceedings of the 15th International Workshop on Satisfiability Modulo Theories (SMT’17),
10 pages, aff. with CAV’17, Heidelberg, Germany, 2017.
[PDF]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2017.
Technical Report 17/1, June 2017,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Aina Niemetz.
Bit Precise Reasoning Beyond Bit-Blasting.
Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2017.
[PDF]
[BibTex]
Mathias Preiner.
Lambdas, Arrays and Quantifiers.
Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2017.
[PDF]
[BibTex]
Mathias Preiner, Aina Niemetz, Armin Biere.
Counterexample-Guided Model Synthesis.
In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17),
Lecture Notes in Computer Science,
volume 10205,
pages 264-280,
Springer, 2017.
[PDF]
[DOI]
[BibTex]
[Artifact]
Aina Niemetz, Mathias Preiner, Armin Biere.
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
In Proceedings of the 28th International Conference on Computer Aided Verification (CAV’16),
Part I,
Lecture Notes in Computer Science,
volume 9779,
pages 199-217,
Springer 2016.
[PDF]
[DOI]
[BibTex]
[Artifact]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2016.
Technical Report 16/1, June 2016,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Mathias Preiner, Aina Niemetz, Armin Biere.
Better Lemmas with Lambda Extraction.
In Proceedings of the 15th
International Conference on Formal Methods in Computer Aided Design (FMCAD’15),
pages 128-135,
FMCAD Inc. 2015.
[PDF]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich.
Improving Local Search For Bit-Vector Logics in SMT with Path Propagation.
In Proceedings of the 4th International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS’15),
10 pages, aff. to FMCAD’15, Austin, TX, USA, 2015.
[PDF]
[BibTex]
[Artifact]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2015.
Technical Report 15/1, June 2015,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector 2.0.
In Journal of Satisfiability, Boolean Modeling and Computation (JSAT),
volume 9, 2015, pages 53-58.
[PDF]
[DOI]
[BibTex]
Aina Niemetz, Mathias Preiner, Armin Biere.
Turbo-Charging Lemmas on Demand with Don’t Care Reasoning.
In Proceedings of the 14th
International Conference on Formal Methods in Computer Aided Design (FMCAD’14),
pages 179-186,
FMCAD Inc, 2014.
[PDF]
[DOI]
[BibTex]
[Artifact]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2014.
Technical Report 14/1, June 2014,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Mathias Preiner, Aina Niemetz, Armin Biere.
Lemmas on Demand for Lambdas.
In Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems,
10 pages, aff. to FMCAD’13, Portland, Oregon, USA, 2013.
[PDF]
[BibTex]
[Artifact]
Armin Biere.
Boolector Entering the SMT Competition 2012.
Technical Report 12/1, June 2012,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Armin Biere.
Boolector at the SMT Competition 2011.
Technical Report 11/3, June 2011,
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[PDF]
[BibTex]
Robert Brummayer.
Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays.
Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2009.
[PDF]
[BibTex]
Robert Brummayer, Armin Biere.
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.
In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’09),
Lecture Notes in Computer Science,
volume 5505,
Springer, 2009.
[PDF]
[BibTex]
Robert Brummayer, Armin Biere.
Lemmas on Demand for the Extensional Theory of Arrays.
In Journal on Satisfiability, Boolean Modeling and Computation (JSAT),
volume 6,
pages 165-201,
Delft University, 2009.
[PDF]
[BibTex]
Robert Brummayer, Armin Biere, Florian Lonsing.
BTOR: Bit-Precise Modeling of Word-Level Problems for Model Checking.
In Proceedings of the 1st International Workshop on Bit-Precise Reasoning (BPR’08),
Princeton, New Jersey, USA, July 2008.
[PDF]
[BibTex]
Robert Brummayer, Armin Biere.
Lemmas on Demand for the Extensional Theory of Arrays.
In Proceedings 6th International Workshop on Satisfiability Modulo Theories (SMT’08),
Princeton, New Jersey, USA, July 2008.
[PDF]
[BibTex]
Andreas Vida.
Random Test Case Generation and Delta Debugging for BitVector Logic with Arrays.
Master Thesis, Johannes Kepler University, October 2008.
[PDF]
[Tool]