ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS

DOI10.1142/S0129054113500123zbMath1286.68319OpenAlexW2099560526MaRDI QIDQ2856015

Alessio Lomuscio, Ben Strulo, Peng Wu, Nigel G. Walker

Publication date: 23 October 2013

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s0129054113500123

zbMATH Keywords

distributed systemcompositional model checkingassume-guarantee reasoning

Mathematics Subject Classification ID

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

Related Items (2)

A weakness measure for GR(1) formulae ⋮ A weakness measure for GR(1) formulae

Cites Work

• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Automatic symbolic compositional verification by learning assumptions
• A proof method for cyclic programs
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
• Linear-time temporal logics with Presburger constraints: an overview ★
• Tentative steps toward a development method for interfering programs
• Proofs of Networks of Processes
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages

This page was built for publication: ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS