Craig Interpolation for Linear Temporal Languages

Model checking technique can give a specific counterexample which explains how the system violates some assertion when model does not satisfy the specification. However, it is a tedious work to understand the long counterexamples. We propose a genetic algorithm to enhance the efficiency of understanding long counterexample by computing the minimal unsatisfiable subformula. Besides, we also propose a Craig interpolation computation-based method to understand counterexample. The causes which are responsible for model failure are extracted by deriving interpolation from the proof of the nonsatisfiability of the initial state and the weakest precondition of counterexample. Experimental results show that our methods improve the efficiency of understanding counterexamples and debugging significantly.

Download Full-text

Random Model Sampling: Making Craig Interpolation Work When It Should Not

Modeling and Analysis of Information Systems ◽

10.18255/1818-1015-2014-6-7-17 ◽

2014 ◽

Vol 21 (6) ◽

pp. 7-17

Author(s):

Marat Akhin ◽

Sam Kolton ◽

Vladimir Itsykson

Keyword(s):

Random Model ◽

Craig Interpolation

Download Full-text

Von Wright’s truth-logic and around

Logical Investigations ◽

10.21146/2074-1472-2013-19-0-39-50 ◽

2013 ◽

Vol 19 ◽

pp. 39-50

Author(s):

А.С. Карпенко

Keyword(s):

Modal Logic ◽

Interpolation Property ◽

Tense Logic ◽

Craig Interpolation ◽

Craig Interpolation Property ◽

Truth Logic

In this paper von Wright’s truth-logic T__ is considered. It seems that it is a De Morgan four-valued logic DM4 (or Belnap’s four-valued logic) with endomorphism e2. In connection with this many other issues are discussed: twin truth operators, a truth-logic with endomorphism g (or logic Tr), the lattice of extensions of DM4, modal logic V2, Craig interpolation property, von Wright–Segerberg’s tense logic W, and so on.

Download Full-text

Craig Interpolation for the Integers: Results, Implementation, and Experiences

10.29007/9rxz ◽

2018 ◽

Author(s):

Philipp Rümmer

Keyword(s):

Model Checking ◽

Formal Verification ◽

Safety Analysis ◽

Craig Interpolation ◽

Integer Arithmetic ◽

Theorem Provers ◽

Smt Solvers ◽

Versatile Tool ◽

Runtime Infrastructure

Craig interpolation is a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. Over the last years, a variety of interpolation procedures for linear integer arithmetic (and extensions) have been developed. I will give an overview of the existing algorithms and design choices, and then discuss implementations of such procedures within theorem provers and SMT solvers. In particular, I will describe an implementation done using the multi-paradigm language Scala, which is built on top of the Java runtime infrastructure, and evaluate performance and engineering aspects.

Download Full-text