ABSTRACT. In the last two decades, Craig interpolation has emerged as an essential tool in formal verification, where first-order theories are used to express constraints on the system, such as on the datatypes manipulated by programs. Interpolants for such theories are largely exploited as an efficient method to approximate the reachable states of the system and for invariant synthesis. In this talk, we report recent results on a stronger form of interpolation, called uniform interpolation, and its connection with the notion of model completion from model-theoretic algebra. In addition, we discuss how uniform interpolants can be used in the context of formal verification of infinite-state systems to develop effective techniques for computing the reachable states in an exact way. Finally, we present some results about the transfer of uniform interpolants to theory combinations. We argue that methods based on uniform interpolation are particularly effective and computationally efficient when applied to safety verification of the so-called data-aware processes: these are systems where the control flow of a (business) process can interact with a data storage.

ABSTRACT. We present a number of algebraic results that facilitate the study of the deductive interpolation property and closely-related metalogical properties for algebraizable deductive systems. We prove that, when V is a congruence-distributive variety, V has the congruence extension property if and only if the class of finitely subdirectly irreducible members of V has the congruence extension property. When a deductive system is algebraized by V, this provides a description of local deduction theorems in terms of algebraic models. Further, we prove that for a variety V with the congruence extension property such that the class of finitely subdirectly irreducibles is closed under subalgebras, V has a one-sided amalgamation property (equivalently, since V is a variety, the amalgamation property) if and only if the class of finitely subdirectly irreducibles has this property. When V is the algebraic counterpart of a deductive system, this yields a characterization of the deductive interpolation property in terms of algebraic semantics. We announce a similar result for the transferable injections property, and prove that possession of all these properties is decidable for finitely generated varieties satisfying certain conditions. Finally, as a case study, we describe the subvarieties of a notable variety of BL-algebras that have the amalgamation property.

ABSTRACT. From a proof-theoretic perspective, the idea that interpolation is tied to provability is a natural one. Thinking about Craig interpolation, if a ‘nice’ proof of a valid implication ϕ→ψ is available, one may succeed in defining an interpolant by induction on the proof-tree, starting from leaves and proceeding to the implication at the root. This method has recently been applied even to fixed point logics admitting cyclic proofs. In contrast, for uniform interpolation, there is no single proof to work from but a collection of proofs to accommodate: a witness to each valid implication ϕ→ψ where the vocabulary of ψ is constrained. Working over a set of prospective proofs and relying on the structural properties of sequent calculus is the essence of Pitts' seminal result on uniform interpolation for intuitionistic logic.

In this talk we will look at how Pitts' technique can be adapted to derive uniform interpolation for the propositional modal μ-calculus. For this we introduce the notion of an interpolation template, a finite (cyclic) derivation tree in a sequent calculus based on the Jungteerapanich-Stirling annotated proof system. Uniform interpolants arise from encoding the structure of interpolation templates within the syntax of the μ-calculus. We will conclude with a somewhat surprising corollary of the interpolation method via cyclic proofs: a straightforward proof of completeness for Kozen's finitary axiomatisation of the μ-calculus.

ABSTRACT. In this note we present a sound, complete, and cut-free tableau calculus for the logic being a formalisation of a Russell-style theory of DD with the iota-operator used to construct DD, the lambda-operator forming predicate-abstracts, and DD as genuine terms with a restricted right of residence. We show that in this setting we are able to overcome problems typical for Russell's original theory, such as scoping difficulties or undesired inconsistencies. We prove the Craig interpolation property for the proposed theory, which, through the Beth definability property, allows us to check whether an individual constant from a signature has a DD-counterpart under a given theory.

ABSTRACT. Proof-based interpolation can be thought of as a proof transformation that localizes a proof by introducing a cut or lemma. The hope is that such a lemma will be generally useful, for example in synthesizing an inductive proof. Usually, we think of interpolants as a service provided by an automated prover to some higher-level reasoner such as a program verifier. In this talk, however, we will consider interpolation as a proof transformation to be applied during proof search. To motivate this idea, we will first consider CDCL as a transformational proof system, with conflict clauses generated by an interpolating transformation rule. Then we move from ground to quantified clauses. By adding one proof search rule and one interpolating transformation rule, we obtain a stratified CHC solver. Another transformation allows us to obtain more general conflict clauses using interpolation. The proof transformation view allows us to tightly integrate higher-level proof strategies with CDCL. This presents engineering challenges, but has the potential to produce a class of efficient solvers that can exploit the structure of problem instances.

ABSTRACT. Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan’s interpolation-based model checking algorithm from 2003 has received little attention in the software-verification community. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.

ABSTRACT. This lecture is about networks consisting of a directed graph in which each vertex is equipped with a language with the Craig interpolation property, along with a knowledge base (set of sentences) in that language. The knowledge bases grow over time according to some set of rules including the following: For any edge between two vertices, any sentence in the first knowledge base that is in the common language can be added to the second knowledge base (intuitively, the first vertex sends a message to the second). We survey a variety of results and problems that arise in this framework. A central question is: Under which conditions will a sentence be eventually provable from the knowledge base at a given vertex.

ABSTRACT. Interference-based proof systems are necessary for proof generation in inprocessing SAT solvers. Unfortunately, their structure and semantic invariants are incompatible with standard recursive interpolant systems. Recent research on interference connects it with inference in more expressive logics. This circumvents some of the roadblocks in the quest for interpolant extraction from interference-based proofs, but also raises questions about the applicability of unfeasibility results in this setting.