Model Checking Recursive Programs with Exact Predicate Abstraction

DOI10.1007/978-3-540-88387-6_9MaRDI QIDQ3540067zbMATH OpenOpenAlexFDO

Authors Arie Gurfinkel, Ou Wei, Marsha Chechik

Publication date 20 November 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-88387-6_9

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Predicate Abstraction of Programs with Non-linear Computation
• LTL model checking for recursive programs
• Predicate Abstraction with Under-approximation Refinement
• SMT-based model checking for recursive programs

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 108368 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 2102712 (Why is no real title available?)
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
• Abstract Interpretation Frameworks
• Algebraic Methodology and Software Technology
• Computer Aided Verification
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation
• Horn clause solvers for program verification
• Verification by gambling on program slices
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
• Abstract interpretation of recursive logic definitions for efficient runtime assertion checking
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements
• Reducing behavioural to structural properties of programs with procedures

Describes a project that uses

Uses Software

• YASM
• Bebop
• CVC Lite
• CUDD
• SPIN

This page was built for publication: Model Checking Recursive Programs with Exact Predicate Abstraction

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