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 Extended Version Artifact

. 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

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

PDF BibTeX

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

PDF BibTeX Arxiv

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:

My work in CVC4 contributed to the following awards:

Solving Quantified Bit-Vectors Using Invertibility Conditions
Jul 17, 2018
Practical SMT Session (SAT/SMT/AR Summer School 2018)
Jul 4, 2018
Counterexample-Guided Model Synthesis
Jul 22, 2017

Contact