Automated Assume-Guarantee Reasoning by Abstraction Refinement

DOI10.1007/978-3-540-70545-1_14MaRDI QIDQ3512489zbMATH OpenOpenAlexFDO

Authors Mihaela Gheorghiu Bobaru, Dimitra Giannakopoulou, Corina S. Păsăreanu

Publication date 15 July 2008

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70545-1_14

Mathematics Subject Classification ID

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

Recommendations

• Automated Assumption Generation for Compositional Verification
• Refining Interface Alphabets for Compositional Verification
• scientific article; zbMATH DE number 1956591
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Automatic symbolic compositional verification by learning assumptions

Cites work

• Automated Assumption Generation for Compositional Verification
• Automated compositional abstraction refinement for concurrent C programs: a two-level approach
• Computer Aided Verification
• Computer Aided Verification
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1283472 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• Learning regular sets from queries and counterexamples
• Optimized L*-Based Assume-Guarantee Reasoning
• Refining Interface Alphabets for Compositional Verification
• SAT-Based Compositional Verification Using Lazy Learning

Cited in

(25)

• Automated circular assume-guarantee reasoning
• Compositional abstraction refinement for control synthesis
• Verification of asynchronous systems with an unspecified component
• To compose, or not to compose, that is the question: an analysis of compositional state space generation
• Compositional verification and 3-valued abstractions join forces
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• scientific article; zbMATH DE number 1701775 (Why is no real title available?)
• Assume-guarantee reasoning with local specifications
• Modular verification of higher-order functional programs
• Automata learning with automated alphabet abstraction refinement
• Compositional reasoning
• Abstraction and abstraction refinement
• Interpolation-based GR(1) assumptions refinement
• scientific article; zbMATH DE number 4213463 (Why is no real title available?)
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement
• scientific article; zbMATH DE number 2086947 (Why is no real title available?)
• Compositional CSP traces refinement checking
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• Automated circular assume-guarantee reasoning
• Refining Interface Alphabets for Compositional Verification
• Learning assumptions for compositional verification of timed automata
• APML: an architecture proof modeling language
• Automatic assume-guarantee reasoning for safety and liveness using passive learning
• Compositional verification in rewriting logic

This page was built for publication: Automated Assume-Guarantee Reasoning by Abstraction Refinement

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