Efficient strategies for CEGAR-based model checking

DOI10.1007/S10817-019-09535-XMaRDI QIDQ2209549zbMATH OpenOpenAlexFDO

Authors Ákos Hajdu, Zoltán Micskei

Publication date 2 November 2020

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-019-09535-x

zbMATH Keywords

abstractionCEGARexperimental evaluationformal verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A configurable CEGAR framework with interpolation-based refinements
• Computer Aided Verification
• scientific article; zbMATH DE number 2087616
• Thread-modular counterexample-guided abstraction refinement
• Proof-Guided Underapproximation Widening for Bounded Model Checking

Cites work

• A configurable CEGAR framework with interpolation-based refinements
• A unifying view on SMT-based software verification
• Abstractions from proofs
• An extension of lazy abstraction with interpolation for programs with arrays
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Counterexample-guided abstraction refinement for symbolic model checking
• Empirical software metrics for benchmarking of verification tools
• Generalized property directed reachability
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 2162362 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Lazy abstraction
• Lazy Abstraction with Interpolants
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• Slicing Abstractions
• Splitting via Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017. Proceedings.

Cited in

(6)

• A configurable CEGAR framework with interpolation-based refinements
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Symbolic observation graph-based generation of test paths
• Bottoms up for CHCs: novel transformation of linear constrained Horn clauses to software verification
• CHC-COMP 2023: competition report
• Find, use, and conserve tools for formal methods

Describes a project that uses

Uses Software

• R
• LTSmin
• SMTInterpol
• SatAbs
• Wolverine
• BLAST
• z3
• SLAM
• KLEE
• CPAchecker
• UFO

This page was built for publication: Efficient strategies for CEGAR-based model checking

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