I was involved as (co-)advisor and/or (co-)author in the following software projects and artifacts (among others), many of which are related to published papers. See also my GitHub profile and the GitHub profile of the Upscale project carried out at Stanford.

Pono Model Checker

Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. See here for further information.

Self-Consistency Checking for Hardware Verification

Artifacts related to symbolic quick error detection (SQED) for processor designs and accelerator quick error detection (A-QED) for hardware accelerator designs:

Symbolic Quick Error Detection (SQED)

Accelerator Quick Error Detection (A-QED)


DepQBF is a search-based QBF solver with conflict-driven clause and solution-driven cube learning. Please see here for further information.

QBF Certificate Extraction and Checking

QBFcert is a framework for resolution-based extraction and checking of certificates for QBFs. E.g., it can be used to check proofs produced by DepQBF and extract Skolem/Herbrand functions.

Parallel QBF Solving

  • HordeQBF is a modular and massively parallel QBF solver. It consists of an MPI-based flexible parallelization framework and integrates DepQBF as a core solver. HordeQBF is a joint project of Tomas Balyo and Florian Lonsing. See also the related SAT 2016 tool paper (PDF preprint).
  • MPIDepQBF is an MPI-based parallel QBF solver without knowledge sharing. It implements a master/worker architecture . A worker consists of an instance of the solver DepQBF. The master balances the workload by generating subproblems defined by variable assignments (assumptions), which are solved by the workers. MPIDepQBF is a joint project of Charles Jordan, Lukasz Kaiser, Florian Lonsing, and Martina Seidl. See also the related SAT 2014 tool paper. Source code of MPIDepQBF is available as part of the Toss project. See here for another implementation of the ideas of MPIDepQBF by Charles Jordan.

QBF Preprocessing

  • QRATPre+ is a preprocessor to simplify quantified Boolean formulas (QBFs) given in prenex conjunctive normal form (PCNF). For simplification, QRATPre+ eliminates redundant clauses from the PCNF, or universal literals from clauses. It implements redundancy checking based on the QRAT+ proof system. Source code is available on GitHub. The theory behind QRATPre+ is described in our IJCAR 2018 paper (preprint on arXiv). We also published a related tool paper at SAT 2019.
  • QxBF is a preprocessor for QBFs in prenex CNF based on failed literal detection. The basic idea is to assign some variable as assumption. If boolean constraint propagation (QBCP) yields an empty clause then the negated assumption can be added as a new unit clause to the CNF. Further information and source code can be found here.
  • Failed literal detection for QBF as implemented in QxBF was extended by Allen Van Gelder and Samuel Wood. See also the paper A. Van Gelder, S. B. Wood, F. Lonsing: Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. in Proc. SAT 2012.
  • Bloqqer is a preprocessor for QBFs in prenex CNF which implements techniques such as quantified blocked clause elimination, equivalence reasoning etc. See also the paper A. Biere, F. Lonsing, and M. Seidl. Blocked Clause Elimination for QBF. Source code and further information can be found here.

QBF Generator and Fuzzer

  • BlocksQBF is a generator for random QBFs in QDIMACS format. Source code and further information can be found here.
  • QBFuzz is a fuzzer which generates random QBFs in QDIMACS format. Source code and further information can be found here.

QBF Delta-Debugger

QBFDD is a delta-debugger for QBFs in QDIMACS format. Source code and further information can be found here.


Nenofex (“NEgation NOrmal Form EXpansion”) is an expansion-based QBF solver which operates on negation normal form (NNF). A formula in NNF is represented as a structurally restricted tree. Expansions of variables from the two rightmost quantifier blocks are scheduled based on estimated expansion costs. Further information can be found in our SAT’08 paper. Source code is available from GitHub.