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)
- An implementation of single instruction checking for the RIDECORE Out of Order RISC-V Processor: https://github.com/upscale-project/ridecore-si-checking
- Python-based workflow to generate QED modules from ISA/architecture specifications: https://github.com/upscale-project/sqed-generator
- A demo that shows how to apply SQED to RIDECORE, a RISC-V core, using a generic QED module. The generic QED module reduces the amount of manual work to be done by the verification engineer: https://github.com/upscale-project/generic-sqed-demo
Accelerator Quick Error Detection (A-QED)
- Artifact demonstrating accelerator quick error detection (A-QED) on several designs: https://github.com/upscale-project/aqed-dac2020-results
- Experiments related to our FMCAD 2021 paper “Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition”: https://github.com/upscale-project/aqed-decomp-FMCAD2021
DepQBF
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
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.