My DBLP profile.
My Google Scholar profile.
Recent Publications
Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a total alignment of different executions that facilitates simpler inductive invariants.
We show how this treatment is achieved via a reduction from the verification problem of ∀∗∃∗ hyperproperties to Constrained Horn Clauses (CHCs). Our starting point is a set of universally quantified formulas in first-order logic (modulo theories) that encode the verification of ∀∗∃∗ hyperproperties over infinite-state transition systems. The first-order encoding uses uninterpreted predicates to capture the (1) witness function for existential quantification over traces, (2) alignment of executions, and (3) corresponding inductive invariant. Such an encoding was previously proposed for k-safety properties. Unfortunately, finding a satisfying model for the resulting first-order formulas is beyond reach for modern first-order satisfiability solvers. Previous works tackled this obstacle by developing specialized solvers for the aforementioned first-order formulas. In contrast, we show that the same problems can be encoded as CHCs and solved by existing CHC solvers. CHC solvers take advantage of the unique structure of CHC formulas and handle the combination of quantifiers with theories and uninterpreted predicates more efficiently.
Our key technical contribution is a logical transformation of the aforementioned sets of first-order formulas to equi-satisfiable sets of CHCs. The transformation to CHCs is sound and complete, and applying it to the first-order formulas that encode verification of hyperproperties leads to a CHC encoding of these problems. We implemented the CHC encoding in a prototype tool and show that, using existing CHC solvers for solving the CHCs, the approach already outperforms state-of-the-art tools for hyperproperty verification by orders of magnitude.
We present StHorn, a novel technique for solving the satisfiability problem of CHCs, which works lazily and incrementally
and is guided by the structure of the set of CHCs.
Our technique is driven by the idea that a set of CHCs can be solved in parts, making it an easier problem for the CHC-solver.
Furthermore, solving a set of CHCs can benefit from an interpretation revealed by the solver for its subsets.
Our technique is lazy in that it gradually extends the set of checked CHCs, as needed.
It is incremental in the way it constructs a solution by using satisfying interpretations obtained for previously checked subsets.
In order to capture the structure of the problem, we define an induced CHC hypergraph that precisely corresponds to the set of CHCs.
The paths in this graph are explored and used to select the clauses to be solved.
We implemented StHorn on top of two CHC-solvers, Spacer and Eldarica.
Our evaluation shows that StHorn complements both tools and can solve instances that cannot be solved by the other tools.
We conclude that StHorn can improve upon the state-of-the-art in CHC solving.
Condition synthesis takes a program in which some of the conditions
in conditional branches are missing, and a specification, and automatically infers
conditions to fill-in the holes such that the program meets the specification.
In this paper, we propose COSYN, an algorithm for determining the realizability
of a condition synthesis problem, with an emphasis on proving unrealizability
efficiently. We use the novel concept of a doomed initial state, which is an initial
state that can reach an error state along every run of the program. For a doomed
initial state σ, there is no way to make the program safe by forcing σ (via condi-
tions) to follow one computation or another. COSYN checks for the existence of
a doomed initial state via a reduction to Constrained Horn Clauses (CHC).
We implemented COSYN in SEAHORN using SPACER as the CHC solver and
evaluated it on multiple examples. Our evaluation shows that COSYN outper-
forms the state-of-the-art syntax-guided tool CVC5 in proving both realizability
and unrealizability. We also show that joining forces of COSYN and CVC5 out-
performs CVC5 alone, allowing to solve more instances, faster.
Condition_Synthesis_Realizability_via_Constrained_Horn_Clauses
IC3 is a highly-effective algorithm for formal hardware verification. It cleverly uses a SAT solver to compute an inductive invariant, an over-approximation of reachable states, of a hardware design. The invariant is computed in CNF as a conjunction of lemmas. This CNF representation over state variables, although efficient, leads to an obvious deficiency: IC3 is not effective for designs that do not have a concise CNF invariant over state variables. We show how to remedy this deficiency by extending traditional IC3 to learn invariants not only in terms of state variables, but also in terms of internal signals of the design.
Our proposed method can learn significantly more compact invariants than IC3, while maintaining a highly-efficient CNF representation. We evaluate our technique on several industrial sequential equivalence checking (SEC) problems from IBM, SEC problems derived from designs in the Hardware Model Checking Competition (HWMCC) and SEC problems from academia. In addition, we evaluate it on HWMCC benchmarks. IC3 with internal signals is efficient for SEC and outperforms traditional IC3 on an important class of benchmarks.