Efficient strategies for CEGAR-based model checking
From MaRDI portal
Publication:2209549
DOI10.1007/s10817-019-09535-xzbMath1468.68131OpenAlexW2988671542MaRDI QIDQ2209549
Publication date: 2 November 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09535-x
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An extension of lazy abstraction with interpolation for programs with arrays
- Empirical software metrics for benchmarking of verification tools
- 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. Part II
- A unifying view on SMT-based software verification
- 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. Proceedings
- A Configurable CEGAR Framework with Interpolation-Based Refinements
- Generalized Property Directed Reachability
- Splitting via Interpolants
- Abstractions from proofs
- Counterexample-guided abstraction refinement for symbolic model checking
- Slicing Abstractions
- Lazy abstraction
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Lazy Abstraction with Interpolants
- Lazy Reachability Checking for Timed Automata with Discrete Variables
