Interpolation Properties and SAT-Based Model Checking

DOI10.1007/978-3-319-02444-8_19MaRDI QIDQ5166692zbMATH OpenOpenAlexFDO

Authors Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina

Publication date 8 July 2014

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1212.4650

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Craig interpolation is a widespread method in verification, with important applications such as Predicate Abstraction, CounterExample Guided Abstraction Refinement and Lazy Abstraction With Interpolants. Most state-of-the-art model checking techniques based on interpolation require collections of interpolants to satisfy particular properties, to which we refer as "collectives"; they do not hold in general for all interpolation systems and have to be established for each particular system and verification environment. Nevertheless, no systematic approach exists that correlates the individual interpolation systems and compares the necessary collectives. This paper proposes a uniform framework, which encompasses (and generalizes) the most common collectives exploited in verification. We use it for a systematic study of the collectives and of the constraints they pose on propositional interpolation systems used in SAT-based model checking.

Recommendations

• Interpolation and SAT-based model checking.
• Interpolation and model checking
• Interpolants and Symbolic Model Checking
• Approximation Refinement for Interpolation-Based Model Checking
• Applications and Theory of Petri Nets 2005
• Computer Science Logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Accelerating Interpolation-Based Model-Checking

Cited in

(14)

• Exploiting partial variable assignment in interpolation-based model checking
• Farkas-based tree interpolation
• Interpolant learning and reuse in SAT-based model checking
• PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
• Generalized Craig interpolation for stochastic Boolean satisfiability problems
• Interpolation and model checking
• Interpolants for Linear Arithmetic in SMT
• Interpolation theorems for some variants of LTL
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Intertwined forward-backward reachability analysis using interpolants
• Approximation Refinement for Interpolation-Based Model Checking
• Interpolation and SAT-based model checking.
• SMT-based verification of program changes through summary repair
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

This page was built for publication: Interpolation Properties and SAT-Based Model Checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166692)