Predicate Abstraction for Program Verification

DOI10.1007/978-3-319-10575-8_15zbMath1392.68253OpenAlexW2803616382MaRDI QIDQ3176373

Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_15

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

Model-checking structured context-free languages, Temporal Logic and Fair Discrete Systems, SAT-Based Model Checking, Satisfiability Modulo Theories, Abstraction and Abstraction Refinement, Interpolation and Model Checking, Combining Model Checking and Deduction, Backward symbolic execution with loop folding, Counterexample classification, Unnamed Item, NIL: learning nonlinear interpolants

Uses Software

• SLAM
• SPIN
• CPAchecker
• ACL2s
• Bebop
• UFO
• SLAB
• Threader
• SatAbs
• YOGI
• Wolverine
• Houdini

Cites Work

• An abstract interpretation framework for termination
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• The ACL2 Sedan Theorem Proving System
• Abstraction and Abstraction Refinement
• Combining Model Checking and Data-Flow Analysis
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Size-Change Termination and Transition Invariants
• The size-change principle for program termination
• Lazy abstraction
• Software model checking
• Low-level liquid types
• Counterexample-guided focus
• Nested interpolants
• Transition predicate abstraction and fair termination
• Computer Aided Verification
• Ramsey vs. Lexicographic Termination Proving
• A constraint-based approach to solving games on infinite graphs
• Predicate abstraction and refinement for verifying multi-threaded programs
• Array Abstractions from Proofs
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems
• Lazy Abstraction with Interpolants
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item