Publications

Filter by type:

. Solving Quantified Bit-Vectors Using Invertibility Conditions. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, 2018.

PDF BibTeX DOI Extended Version Artifact CVC4

. Btor2 , BtorMC and Boolector 3.0. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, 2018.

PDF BibTeX DOI Boolector

. Rewrites for SMT Solvers using Syntax-Guided Enumeration. Proceedings of the 16th International Workshop on Satisfiability Modulo Theories, SMT 2018), affiliated with the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK, July 12-13, 2018, 2018.

PDF BibTeX CVC4

. CVC4 at the SMT Competition 2018. CoRR abs/1806.08775, 2018.

PDF BibTeX Arxiv CVC4

. Boolector at the SMT competition 2018. FMV Reports Series, Technical Report 18/1, 2018.

PDF BibTeX Boolector

. Propagation based local search for bit-precise reasoning. Formal Methods in System Design, 2017.

Preprint PDF BibTeX DOI Artifact Boolector

. Model-Based API Testing for SMT Solvers. Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017, affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, July 24-28, 2017, 2017.

PDF BibTeX Boolector

. Boolector at the SMT competition 2017. FMV Reports Series, Technical Report 17/1, 2017.

PDF BibTeX Boolector

. Counterexample-Guided Model Synthesis. Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, 2017.

PDF BibTeX DOI Artifact Boolector

. Bit-Precise Reasoning Beyond Bit-Blasting. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University Linz, 2017.

PDF BibTeX Boolector ddSMT

. Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, 2016.

PDF BibTeX DOI Artifact Boolector

. Boolector at the SMT competition 2016. FMV Reports Series, Technical Report 16/1, 2016.

PDF BibTeX Boolector

. Better Lemmas with Lambda Extraction. Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015., 2015.

PDF BibTeX Boolector

. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS’15), 2015.

PDF BibTeX Artifact Boolector

. Boolector at the SMT competition 2015. FMV Reports Series, Technical Report 15/1, 2015.

PDF BibTeX Boolector

. Boolector 2.0 system description. Journal on Satisfiability, Boolean Modeling and Computation, 2015.

PDF BibTeX Boolector

. Turbo-charging Lemmas on demand with don't care reasoning. Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, 2014.

PDF BibTeX DOI Artifact Boolector

. Boolector at the SMT competition 2014. FMV Report Series, Technical Report 14/1, 2014.

PDF BibTeX Boolector

. Lemmas on Demand for Lambdas. Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, Portland, OR, USA, October 19, 2013., 2013.

PDF BibTeX Artifact Boolector

. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, SMT 2013), affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, July 8-9, 2013, 2013.

PDF BibTeX ddSMT

. Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. POS-13. Fourth Pragmatics of SAT workshop, a workshop of the SAT 2013 conference, July 7, 2013, Helsinki, Finland, 2013.

PDF BibTeX

. Resolution-Based Certificate Extraction for QBF - (Tool Presentation). Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, 2012.

PDF BibTeX DOI QBFcert

. Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF Solver. Master’s Thesis, Informatik, Johannes Kepler University Linz, 2012.

PDF BibTeX QBFcert