-
Article
Abstract Interpretation as Automated Deduction
Automata theory, algorithmic deduction and abstract interpretation provide the foundation behind three approaches to implementing program verifiers. This article is a first step towards a mathematical translat...
-
Chapter and Conference Paper
Complete Abstractions and Subclassical Modal Logics
Forwards-completeness is a concept in abstract interpretation expressing that an abstract and a concrete transformer have the same semantics with respect to an abstraction. When the set of transformers is gene...
-
Chapter and Conference Paper
Independence Abstractions and Models of Concurrency
Mathematical representations of concurrent systems rely on two fundamental notions: an atomic unit of behaviour called an event, and a constraint called independence which asserts that the order in which certa...
-
Chapter and Conference Paper
Abstract Interpretation with Unfoldings
We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures...
-
Chapter and Conference Paper
Conflict-Driven Conditional Termination
Conflict-driven learning, which is essential to the performance of sat and smt solvers, consists of a procedure that searches for a model of a formula, and refutation procedure for proving that no model exists. T...
-
Chapter and Conference Paper
Abstract Interpretation as Automated Deduction
Algorithmic deduction and abstract interpretation are two widely used and successful approaches to implementing program verifiers. A major impediment to combining these approaches is that their mathematical fo...
-
Article
Open AccessDeciding floating-point logic with abstract conflict driven clause learning
We present a bit-precise decision procedure for the theory of floating-point arithmetic. The core of our approach is a non-trivial, lattice-theoretic generalisation of the conflict-driven clause learning algor...
-
Chapter and Conference Paper
Generalizing Simulation to Abstract Domains
We introduce a notion of subsumption for domains used in abstract interpretation. We show that subsumption has the same properties and applications in the context of abstract interpretation that simulation has...
-
Chapter and Conference Paper
An Abstract Interpretation of DPLL(T)
dpll(t) is a central algorithm for Satisfiability Modulo Theories (smt) solvers. The algorithm combines results of reasoning about the Boolean structure of a formula with reasoning about conjunct...
-
Chapter and Conference Paper
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
One approach for smt solvers to improve efficiency is to delegate reasoning to abstract domains. Solvers using abstract domains do not support interpolation and cannot be used for interpolation-based verification...
-
Chapter and Conference Paper
Abstraction of Syntax
The theory of abstract interpretation is a conceptual framework for reasoning about approximation of semantics. We ask if the creative process of designing an approximation can be studied mathematically. Seman...
-
Chapter and Conference Paper
Numeric Bounds Analysis with Conflict-Driven Learning
This paper presents a sound and complete analysis for determining the range of floating-point variables in control software. Existing approaches to bounds analysis either use convex abstract domains and are ef...
-
Chapter and Conference Paper
Satisfiability Solvers Are Static Analysers
This paper shows that several propositional satisfiability algorithms compute approximations of fixed points using lattice-based abstractions. The Boolean Constraint Propagation algorithm (bcp) is a greatest f...
-
Article
A lazy approach to symmetry reduction
Symmetry reduction is a technique to counter state explosion for systems with regular structure. It relies on idealistic assumptions about indistinguishable components, which in practice may only be similar. In t...
-
Chapter and Conference Paper
Propositional Interpolation and Abstract Interpretation
Algorithms for computing Craig interpolants have several applications in program verification. Though different algorithms exist, the relationship between them and the properties of the interpolants they gener...
-
Chapter and Conference Paper
Interpolant Strength
Interpolant-based model checking is an approximate method for computing invariants of transition systems. The performance of the model checker is contingent on the approximation computed, which in turn depends...
-
Chapter and Conference Paper
Approximation Refinement for Interpolation-Based Model Checking
Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from ...
-
Chapter and Conference Paper
A Toolset for Modelling and Verification of GALS Systems
We present a toolset for design and verification of Globally Asynchronous Locally Synchronous(GALS) systems. Such systems consist of a network of reactive nodes which have independent clocks and I/O interfaces...
