Automated Assume-Guarantee Reasoning by Abstraction Refinement

DOI10.1007/978-3-540-70545-1_14zbMath1155.68435OpenAlexW1801993675MaRDI QIDQ3512489

Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, 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)

Related Items (15)

Compositional Reasoning ⋮ Abstraction and Abstraction Refinement ⋮ Automated circular assume-guarantee reasoning ⋮ Compositional abstraction refinement for control synthesis ⋮ Modular Verification of Higher-Order Functional Programs ⋮ Verification of asynchronous systems with an unspecified component ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ Compositional verification and 3-valued abstractions join forces ⋮ To compose, or not to compose, that is the question: an analysis of compositional state space generation ⋮ Learning assumptions for compositional verification of timed automata ⋮ APML: an architecture proof modeling language ⋮ Automated Circular Assume-Guarantee Reasoning ⋮ Automata Learning with Automated Alphabet Abstraction Refinement ⋮ ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS ⋮ A framework for compositional verification of multi-valued systems via abstraction-refinement

Cites Work

• Learning regular sets from queries and counterexamples
• SAT-Based Compositional Verification Using Lazy Learning
• Automated Assumption Generation for Compositional Verification
• Computer Aided Verification
• Computer Aided Verification
• Refining Interface Alphabets for Compositional Verification
• Optimized L*-Based Assume-Guarantee Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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