Software Verification with PDR: An Implementation of the State of the Art

DOI10.1007/978-3-030-45190-5_1OpenAlexW3016403159MaRDI QIDQ5039500

Dirk Beyer, Matthias Dangl

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1908.06271

zbMATH Keywords

program analysissoftware verificationinvariant generation\(k\)-inductionIC3CPAcheckerproperty-directed reachability (PDR)VVT

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Backward symbolic execution with loop folding

Uses Software

• SLAM
• CPAchecker
• SeaHorn
• PKind
• BOXES
• CTIGAR

Cites Work

• Unnamed Item
• Property-directed incremental invariant generation
• A unifying view on SMT-based software verification
• Infinite-state invariant checking with IC3 and predicate abstraction
• SAT-Based Model Checking without Unrolling
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Counterexample-guided abstraction refinement for symbolic model checking
• Boxes: A Symbolic Abstract Domain of Boxes
• Software model checking
• Improving Generalization in Software IC3
• Computer Aided Verification

This page was built for publication: Software Verification with PDR: An Implementation of the State of the Art