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

DOI10.1007/978-3-540-75596-8_40zbMath1141.68489OpenAlexW2097257018MaRDI QIDQ3510827

Masahiro Fujita, Thanyapat Sakunkonchak, Satoshi Komatsu

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)

Uses Software

• veriSoft
• BLAST
• SLAM

Cites Work

• Predicate abstraction of ANSI-C programs using SAT
• Verification of SpecC using predicate abstraction
• Abstractions from proofs
• Precise interprocedural dataflow analysis with applications to constant propagation
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item

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