Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning

DOI10.1007/s10703-008-0049-6zbMath1147.68053OpenAlexW2117013774MaRDI QIDQ934706

Mihaela Gheorghiu Bobaru, Corina S. Păsăreanu, Dimitra Giannakopoulou, Jamieson M. Cobleigh, Howard Barringer

Publication date: 30 July 2008

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-008-0049-6

zbMATH Keywords

LearningModel checkingAssume-guarantee reasoningCompositional verificationLabeled transition systemsProof rulesSafety properties

Mathematics Subject Classification ID

Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (16)

Assume, Guarantee or Repair ⋮ Compositional Reasoning ⋮ Inferring regular languages and \(\omega\)-languages ⋮ Automated circular assume-guarantee reasoning ⋮ Compositional probabilistic verification through multi-objective model checking ⋮ Automated program repair using formal verification techniques ⋮ Inferring Symbolic Automata ⋮ Verification of asynchronous systems with an unspecified component ⋮ Compositional model checking for multi-properties ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ To compose, or not to compose, that is the question: an analysis of compositional state space generation ⋮ Automated Circular Assume-Guarantee Reasoning ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ Unnamed Item ⋮ ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS ⋮ A framework for compositional verification of multi-valued systems via abstraction-refinement

Uses Software

• NuSMV
• MOCHA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Learning regular sets from queries and counterexamples
• Inference of finite automata using homing sequences
• Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
• Synthesis of interface specifications for Java classes
• SAT-Based Compositional Verification Using Lazy Learning
• Computer Aided Verification
• FM 2005: Formal Methods
• Refining Interface Alphabets for Compositional Verification
• Optimized L*-Based Assume-Guarantee Reasoning

This page was built for publication: Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning