10 citations · 14 across the 3 of their papers we have counts for
7 papers · 1 filter
A Theoretical Framework for Symbolic Quick Error Detection
Florian Lonsing, Subhasish Mitra, Clark Barrett
Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for…
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
Florian Lonsing, Uwe Egly
We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong…
Expansion-Based QBF Solving Without Recursion
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic +3
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional…
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Florian Lonsing, Uwe Egly
The QRAT (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning to…
Q-Resolution with Generalized Axioms
Florian Lonsing, Uwe Egly, Martina Seidl
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learnin…
Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
Roderick Bloem, Uwe Egly, Patrick Klampfl +3
Existing approaches to synthesize reactive systems from declarative specifications mostly rely on Binary Decision Diagrams (BDDs), inheriting their scalability issues. We present n…