[  17 | 16 | 15 | 14 | 13 | 12 ]

2017

Aina Niemetz, Mathias Preiner, Armin Biere. Propagation based local search for bit-precise reasoning . In Journal of Formal Methods in System Design, vol. 51(3), pages 608-636, Springer 2017.
[ paper | preprint | experiments ]

Aina Niemetz, Mathias Preiner, Armin Biere. Model-Based API Testing for SMT Solvers. In Proc. 15th Intl. Workshop on Satisfiability Modulo Theories (SMT'17), 10 pages, aff. to CAV'17, Heidelberg, Germany, 2017.
[ paper | bibtex | boolector ]

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.
[ report | bibtex | boolector ]

Mathias Preiner. Lambdas, Arrays and Quantifiers. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2017.
[ thesis | bibtex ]

Mathias Preiner, Aina Niemetz, Armin Biere. Counterexample-Guided Model Synthesis. In Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Lecture Notes in Computer Science (LNCS) vol. 10205, pages 264-280, Springer 2017.
[ paper | bibtex | data | boolector ]

2016

Aina Niemetz, Mathias Preiner, Armin Biere. Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. In Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16), Lecture Notes in Computer Science (LNCS) vol. 9779, pages 199-217, Springer 2016.
[ paper | bibtex | data | boolector ]

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.
[ report | bibtex | boolector ]

2015

Mathias Preiner, Aina Niemetz, Armin Biere. Better Lemmas with Lambda Extraction. In Proc. 15th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15), pages 128-135, FMCAD Inc. 2015.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. In Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15), 10 pages, aff. to FMCAD'15, Austin, TX, USA, 2015.
[ paper | bibtex | data ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector 2.0. Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, 2015, pages 53-58.
[ paper | bibtex | boolector ]

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.
[ report | bibtex | boolector ]

2014

A. Niemetz, M. Preiner, A. Biere. Turbo-Charging Lemmas on Demand with Don't Care Reasoning In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 179-186, FMCAD Inc, 2014.
[ paper | bibtex | data | boolector ]

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.
[ report | bibtex | boolector ]

2013

M. Preiner, A. Niemetz, A. 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.
[ paper | bibtex | data | boolector ]

M. Aigner, A. Biere, C. M. Kirsch, A. Niemetz, M. Preiner. Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. In Proc. Intl. Workshop on Pragmatics of SAT (POS'13), aff. to SAT'13, Helsinki, Finland, 2013.

2012

A. Niemetz, M. Preiner, F. Lonsing, M. Seidl, A. Biere. Resolution-Based Certificate Extraction for QBF (Tool Presentation). In Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Lecture Notes in Computer Science (LNCS) vol. 7317, pages 430-435, Springer 2012.
[ paper | bibtex | qbfcert ]

M. Preiner, Extracting and Validating Skolem/Herbrand Function-Based QBF Certificates. Master's thesis, Johannes Kepler University Linz, Austria, May 2012.