Publications

(2019). Towards Bit-Width-Independent Proofs in SMT Solvers. Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings.

PDF DOI Arxiv

(2019). Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings.

PDF DOI Preprint

(2019). Invertibility Conditions for Floating-Point Formulas. Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II.

PDF DOI Preprint Extended Version Artifact

(2019). DRAT-based Bit-Vector Proofs in CVC4. Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings.

PDF DOI Arxiv

(2019). Boolector at the SMT competition 2019. 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

(2018). 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.

PDF DOI Preprint Extended Version Artifact

(2018). 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.

PDF

(2018). 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.

PDF DOI Preprint

(2017). 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.

PDF

(2017). Lambdas, Arrays and Quantifiers. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University Linz.

PDF

(2017). 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.

PDF DOI Preprint Artifact

(2016). 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.

PDF DOI Preprint Artifact

(2015). 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).

PDF Artifact

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

PDF

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

PDF DOI Preprint Artifact

(2013). 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..

PDF Artifact

(2013). 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.

PDF

(2012). 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.

PDF DOI