Recent Publications

More Publications

. 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

. 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 I, 2018.

PDF BibTeX DOI

. Propagation Based Local Search for Bit-Precise Reasoning. Formal Methods in System Design, 2017.

PDF BibTeX DOI

. Boolector at the SMT Competition 2017. 2017.

PDF BibTeX

. 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

Projects/Tools

Boolector

An efficient SMT solver for the theory fixed-size bit-vectors with arrays and uninterpreted functions.

Cvc4

An efficient automatic theorem prover for SMT, which supports many different theories and their combination.

QBFcert

A framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).

QBFuzz

A fuzzer for quantified boolean formulas (QBF) in QDIMACS format.

QxBF

A QBF preprocessor based on failed literal detection.

Awards

My work in Boolector contributed to the following awards:

Counterexample-Guided Model Synthesis
Jul 22, 2017
Counterexample-Guided Model Synthesis
Apr 25, 2017
Counterexample-Guided Model Synthesis for Quantified Bit-Vectors
Nov 18, 2016
Better Lemmas with Lambda Extraction
Sep 29, 2015
Lemmas on Demand for Lambdas
Oct 19, 2013

Contact