A configurable CEGAR framework with interpolation-based refinements

DOI10.1007/978-3-319-39570-8_11zbMATH Open1347.68226OpenAlexW2474905024WikidataQ57086291 ScholiaQ57086291MaRDI QIDQ2827465FDOQ2827465

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

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

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)

Cites Work

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

Cited In (2)

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

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)