Three optimizations for assume-guarantee reasoning with L^*

DOI10.1007/S10703-007-0042-5MaRDI QIDQ934701zbMATH OpenOpenAlexFDO

Authors Sagar Chaki, Ofer Strichman

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-007-0042-5

zbMATH Keywords

Assume-GuaranteeCompositionalityLearningSoftware verification

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

• Optimized L*-Based Assume-Guarantee Reasoning
• 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

Cites work

• Approximation algorithms for combinatorial problems
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Counterexample-guided abstraction refinement for symbolic model checking
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 2080060 (Why is no real title available?)
• scientific article; zbMATH DE number 1418458 (Why is no real title available?)
• Inference of finite automata using homing sequences
• Learning regular sets from queries and counterexamples
• Regular model checking using inference of regular languages
• Synthesis of interface specifications for Java classes

Cited in

(6)

• Compositional reasoning
• SAT-Based Compositional Verification Using Lazy Learning
• Computer Aided Verification
• Optimized L*-Based Assume-Guarantee Reasoning
• Learning assumptions for compositional verification of timed automata
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning

Describes a project that uses

Uses Software

• PBS
• ComFoRT

This page was built for publication: Three optimizations for assume-guarantee reasoning with \(L^{*}\)

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