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

(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

(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

(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

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

(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

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

(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

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

(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

(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

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

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

(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

(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

(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