Automated circular assume-guarantee reasoning

DOI10.1007/S00165-017-0436-0zbMath1395.68184OpenAlexW3022825686MaRDI QIDQ1673656

Karam Abd Elkader, Sharon Shoham, Orna Grumberg, Corina S. Păsăreanu

Publication date: 12 September 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0436-0

zbMATH Keywords

model checkingassume-guaranteecircular assume-guaranteeSAT-based assume-guarantee

Mathematics Subject Classification ID

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

Cites Work

• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Automated assumption generation for compositional verification
• Learning regular sets from queries and counterexamples
• Exact learning Boolean functions via the monotone theory
• Counterexample-guided abstraction refinement for symbolic model checking
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Learning Minimal Separating DFA’s for Compositional Verification
• Proofs of Networks of Processes
• Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement
• Synthesis of Circular Compositional Program Proofs via Abduction
• An axiomatic basis for computer programming
• 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

This page was built for publication: Automated circular assume-guarantee reasoning