Predicate Abstraction in Program Verification: Survey and Current Trends

DOI10.4230/OASIcs.ICCSW.2014.27zbMath1427.68165OpenAlexW2110866486MaRDI QIDQ5240105

Jakub Daniel, Pavel Parizek

Publication date: 24 October 2019

Full work available at URL: https://dblp.uni-trier.de/db/conf/iccsw/iccsw2014.html#DanielP14

zbMATH Keywords

model checkingrefinementprogram verificationpredicate abstraction

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• BLAST
• CPAchecker
• SLAyer
• SatAbs
• SAFARI

Cites Work

• Unnamed Item
• Unnamed Item
• From Low-Level Pointers to High-Level Containers
• Lazy Abstraction with Interpolants for Arrays
• From Under-Approximations to Over-Approximations and Back
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Abstractions from proofs
• Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
• Lazy abstraction
• Array Abstractions from Proofs
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Lazy Abstraction with Interpolants

This page was built for publication: Predicate Abstraction in Program Verification: Survey and Current Trends