Progress in Certifying Hardware Model Checking Results

We present a formal framework to certify k-induction-based model checking results. The key idea is the notion of a k-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present Certifaiger, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.

From QBFs to MALL and Back via Focussing

In this work we investigate how to extract alternating time bounds from ‘focussed’ proof systems. Our main result is the obtention of fragments of $$\mathsf {MALL} {\mathsf {w} }$$ MALL w ($$\mathsf {MALL} $$ MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of $$\mathsf {MALL} {\mathsf {w} }$$ MALL w into $$\mathsf {MALL} $$ MALL , we obtain a similar delineation of $$\mathsf {MALL} $$ MALL formulas, again carving out fragments complete for each level of the polynomial hierarchy. This refines the well-known results that both $$\mathsf {MALL} {\mathsf {w} }$$ MALL w and $$\mathsf {MALL} $$ MALL are $$\mathbf {PSPACE}$$ PSPACE -complete. A key insight is that we have to refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch. This is so that we may more faithfully associate phases of focussed proof search to their alternating time complexity. This presentation seems to uncover further dualities, at the level of proof search, than usual presentations, so could be of proof theoretic interest in its own right.

AN ALGEBRAIC APPROACH TO MSO-DEFINABILITY ON COUNTABLE LINEAR ORDERINGS

We develop an algebraic notion of recognizability for languages of words indexed by countable linear orderings. We prove that this notion is effectively equivalent to definability in monadic second-order (MSO) logic. We also provide three logical applications. First, we establish the first known collapse result for the quantifier alternation of MSO logic over countable linear orderings. Second, we solve an open problem posed by Gurevich and Rabinovich, concerning the MSO-definability of sets of rational numbers using the reals in the background. Third, we establish the MSO-definability of the set of yields induced by an MSO-definable set of trees, confirming a conjecture posed by Bruyère, Carton, and Sénizergues.

Anatomy of Alternating Quantifier Satisfiability (Work in progress)

We report on work in progress to generalize an algorithm recently introduced in [10] for checkingsatisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminatingor partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmeticformulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report onexperiments on different variants of the auxiliary procedures. So far, there is an edge to applyingSMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantifiedvariables per round is almost as good. Both approaches offer drastic improvements to applyingdefault quantifier elimination.