Predicate abstraction in program verification: survey and current trends

DOI10.4230/OASICS.ICCSW.2014.27MaRDI QIDQ5240105zbMATH OpenOpenAlexFDO

Authors 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 checkingpredicate abstractionprogram verificationrefinement

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction for program verification
• Verification and falsification of programs with loops using predicate abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction with minimum predicates
• Predicate abstraction of ANSI-C programs using SAT

Cites work

• Abstractions from proofs
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Array Abstractions from Proofs
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• From low-level pointers to high-level containers
• From under-approximations to over-approximations and back
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• Lazy abstraction
• Lazy Abstraction with Interpolants
• Lazy abstraction with interpolants for arrays
• Model checking
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(16)

• A unifying view on SMT-based software verification
• Predicate abstraction of ANSI-C programs using SAT
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• Verification of SpecC using predicate abstraction
• Predicate abstraction for program verification
• Predicate Abstraction of Programs with Non-linear Computation
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• Predicate abstraction for software verification
• Computer Science Logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction and refinement for verifying multi-threaded programs
• Competent predicate abstraction in model checking
• Automated Technology for Verification and Analysis
• Predicate abstraction with minimum predicates
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification and falsification of programs with loops using predicate abstraction

Describes a project that uses

Uses Software

• SLAyer
• SatAbs
• BLAST
• CPAchecker
• SAFARI

This page was built for publication: Predicate abstraction in program verification: survey and current trends

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