A Configurable CEGAR Framework with Interpolation-Based Refinements

DOI10.1007/978-3-319-39570-8_11zbMath1347.68226OpenAlexW2474905024WikidataQ57086291 ScholiaQ57086291MaRDI QIDQ2827465

Ákos Hajdu, András Vörös, Tamás Tóth, István Majzik

Publication date: 19 October 2016

Published in: Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01432916/file/426757_1_En_11_Chapter.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (2)

A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking

Uses Software

• z3

Cites Work

• Splitting via Interpolants
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Abstractions from proofs
• Counterexample-guided abstraction refinement for symbolic model checking
• Slicing Abstractions
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Lazy Abstraction with Interpolants

This page was built for publication: A Configurable CEGAR Framework with Interpolation-Based Refinements