QBF-Based Formal Verification: Experience and Perspectives
Bibliographic record
Abstract
The language of Quantified Boolean Formulas (QBF) has a lot of potential applications to Formal Verification (FV) tasks, as it captures many of these tasks in a natural and compact way.Practical experience has been disappointing though.When compared with contending approaches such as SAT, QBF-based FV has invariably yielded unfavorable experimental results.This paper makes two contributions.We first provide an account of the status quo in QBF-based FV.We examine commonly adopted formalizations and the relative strengths of different decision procedures.In the second part of this paper, we investigate for the first time the relevance of some advanced QBF techniques to FV tasks.In particular, we describe the use and the benefits of restricted quantifiers, QBF certificates, alternative encodings for classical model checking problems, and encodings with free variables.These promising research perspectives seem to reverse the negative standing of QBF applied to FV, as confirmed by the experimental evidence we discuss.Experiments are conducted by extending the publicly available solver sKizzo in several ways, and they include the first case studies where QBF compares favorably to SAT, its traditional competitor.QBF turns out to be an order of magnitude faster than SAT in some tasks (e.g., automated design debugging of large circuits).Moreover, as the size of the problems grows, the SAT encodings result in excessive memory requirements leading to out-of-memory conditions, while the more compact QBF encodings continue to be manageable and solvable.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.035 | 0.027 |
| Meta-epidemiology (narrow) | 0.002 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.002 | 0.002 |
| Science and technology studies | 0.001 | 0.007 |
| Scholarly communication | 0.006 | 0.014 |
| Open science | 0.004 | 0.003 |
| Research integrity | 0.003 | 0.005 |
| Insufficient payload (model declined to judge) | 0.006 | 0.002 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".