Applications of Craig Interpolation to Model Checking

Computer Science Logic - Lecture Notes in Computer Science ◽

10.1007/978-3-540-30124-0_3 ◽

2004 ◽

pp. 22-23 ◽

Cited By ~ 9

Author(s):

Kenneth McMillan

Keyword(s):

Model Checking ◽

Craig Interpolation

Download Full-text

A Fast Approach of Locating Complex System Design Errors

Key Engineering Materials ◽

10.4028/www.scientific.net/kem.572.115 ◽

2013 ◽

Vol 572 ◽

pp. 115-118

Author(s):

Zhi Yuan Chen ◽

Shao Bin Huang ◽

Li Li Han

Keyword(s):

Complex System ◽

Genetic Algorithm ◽

Model Checking ◽

System Design ◽

Experimental Results ◽

Initial State ◽

Craig Interpolation ◽

Fast Approach ◽

Complex System Design ◽

Model Failure

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

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

Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

10.29007/zfkw ◽

2018 ◽

Author(s):

Angelo Brillout ◽

Daniel Kroening ◽

Philipp Rümmer ◽

Thomas Wahl

Keyword(s):

Model Checking ◽

Program Verification ◽

Model Checker ◽

Craig Interpolation ◽

Presburger Arithmetic ◽

C Programs ◽

Full Theory ◽

Software Model ◽

Interpolation Procedure ◽

Versatile Tool

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

Download Full-text

Quantified Heap Invariants for Object-Oriented Programs

10.29007/zrct ◽

2018 ◽

Author(s):

Temesghen Kahsai ◽

Rody Kersten ◽

Philipp Rümmer ◽

Martin Schäf

Keyword(s):

Model Checking ◽

Data Structures ◽

Program Transformation ◽

Object Oriented ◽

Craig Interpolation ◽

Transformation Rules ◽

Java Programs ◽

Software Programs ◽

Inductive Invariants

Heap and data structures represent one of the biggest challenges when applying model checking to the analysis of software programs: in order to verify (unbounded) safety of a program, it is typically necessary to formulate quantified inductive invariants that state properties about an unbounded number of heap locations. Methods like Craig interpolation, which are commonly used to infer invariants in model checking, are often ineffective when a heap is involved. To address this challenge, we introduce a set of new proof and program transformation rules for verifying object-oriented programs with the help of space invariants, which (implicitly) give rise to quantified invariants. Leveraging advances in Horn solving, we show how space invariants can be derived fully automatically, and how the framework can be used to effectively verify safety of Java programs.

Download Full-text