[  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 | bibtex | 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 ]

Aina Niemetz. Bit Precise Reasoning Beyond Bit-Blasting. 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 | boolector ]

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 | boolector ]

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

Aina Niemetz, Mathias Preiner, Armin 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

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

Aina Niemetz, Armin Biere. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 36-45, aff. to SAT'13, Helsinki, Finland, 2013.
[ paper | bibtex | ddsmt ]

Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias 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

Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin 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 ]

Aina Niemetz, Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF-Solver. Master's thesis, Johannes Kepler University Linz, Austria, May 2012.