Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction

DOI10.1007/978-3-540-75596-8_40MaRDI QIDQ3510827zbMATH OpenOpenAlexFDO

Authors Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita

Publication date 3 July 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-75596-8_40

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction with minimum predicates
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1956582

Cites work

• Abstractions from proofs
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• Lazy abstraction
• Precise interprocedural dataflow analysis with applications to constant propagation
• Predicate abstraction of ANSI-C programs using SAT
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of SpecC using predicate abstraction

Cited in

(4)

• Accelerating predicate abstraction by minimum unsatisfiable cores extraction
• scientific article; zbMATH DE number 1979541 (Why is no real title available?)
• Predicate abstraction with minimum predicates
• Making predicate abstraction efficient: how to eliminate redundant predicates

Describes a project that uses

Uses Software

• SLAM
• veriSoft
• BLAST

This page was built for publication: Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction

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