Model Checking Recursive Programs with Exact Predicate Abstraction

DOI10.1007/978-3-540-88387-6_9zbMath1183.68373OpenAlexW1605476801MaRDI QIDQ3540067

Ou Wei, Arie Gurfinkel, 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)

Related Items (3)

Verification by gambling on program slices ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Horn Clause Solvers for Program Verification

Uses Software

• SPIN
• CUDD
• CVC Lite
• Bebop
• YASM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Abstract Interpretation Frameworks
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Algebraic Methodology and Software Technology
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

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