Optimized L*-Based Assume-Guarantee Reasoning

DOI10.1007/978-3-540-71209-1_22MaRDI QIDQ5758116zbMATH OpenOpenAlexFDO

Authors Sagar Chaki, Ofer Strichman

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Three optimizations for assume-guarantee reasoning with \(L^{*}\)
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• SAT-Based Compositional Verification Using Lazy Learning
• Computer Aided Verification
• Computer Aided Verification

Cited in

(14)

• Automated circular assume-guarantee reasoning
• Verification of asynchronous systems with an unspecified component
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• Abstraction and abstraction refinement
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Learning Minimal Separating DFA’s for Compositional Verification
• Assume, guarantee or repair
• Computer Aided Verification
• Automated program repair using formal verification techniques
• Learning assumptions for compositional verification of timed automata
• Three optimizations for assume-guarantee reasoning with \(L^{*}\)
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Automated assumption generation for compositional verification
• Verification of evolving software via component substitutability analysis

This page was built for publication: Optimized L*-Based Assume-Guarantee Reasoning

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