Complexity and Algorithms for Monomial and Clausal Predicate Abstraction

DOI10.1007/978-3-642-02959-2_18MaRDI QIDQ5191104zbMATH OpenOpenAlexFDO

Authors Shuvendu K. Lahiri, Shaz Qadeer

Publication date 28 July 2009

Published in Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02959-2_18

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Predicate Abstraction via Symbolic Decision Procedures
• Computer Aided Verification
• A symbolic approach to predicate abstraction.
• Predicate abstraction for program verification
• Abstractions from proofs

Cites work

• Abstractions from proofs
• Back to the future, revisiting precise program verification using SMT solvers
• Constraint-Based Invariant Inference over Predicate Abstraction
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• Lazy abstraction
• Static Analysis
• Unifying type checking and property checking for low-level code
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• ExplainHoudini: making Houdini inference transparent
• Verification, Model Checking, and Abstract Interpretation
• Invariant inference with provable complexity from the monotone theory
• SAT-based invariant inference and its relation to concept learning

Describes a project that uses

Uses Software

• Houdini
• SMT-LIB

This page was built for publication: Complexity and Algorithms for Monomial and Clausal Predicate Abstraction

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