A configurable CEGAR framework with interpolation-based refinements

DOI10.1007/978-3-319-39570-8_11MaRDI QIDQ2827465zbMATH OpenOpenAlexWikidataFDO

Authors Ákos Hajdu, Tamás Tóth, András Vörös, 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)

Recommendations

• Efficient strategies for CEGAR-based model checking
• Computer Aided Verification
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Thread-modular counterexample-guided abstraction refinement
• Parallel assignments in software model checking

Cites work

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

Cited in

(2)

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

Describes a project that uses

Uses Software

• z3

This page was built for publication: A configurable CEGAR framework with interpolation-based refinements

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