Verification of asynchronous systems with an unspecified component
From MaRDI portal
Publication:1731830
DOI10.1007/s00236-018-0317-xzbMath1417.68096arXiv1709.03245MaRDI QIDQ1731830
Fatemeh Ghassemi, Rosa Abbasi, Ramtin Khosravi
Publication date: 14 March 2019
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1709.03245
68Q60: Specification and verification (program logics, model checking, etc.)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Creol: A type-safe object-oriented model for distributed concurrent systems
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Automatic symbolic compositional verification by learning assumptions
- Learning regular sets from queries and counterexamples
- Recognizing safety and liveness
- Testing equivalences for processes
- Trace and testing equivalence on asynchronous processes
- Compositionality of Hennessy-Milner logic by structural operational semantics
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- On the Construction of Fine Automata for Safety Properties
- Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
- Inferring Network Invariants Automatically
- Process algebra for synchronous communication
- Supervisory Control of a Class of Discrete Event Processes
- Compositionality Through an Operational Semantics of Contexts
- A foundation for actor computation
- Supervisory control using failure semantics and partial specifications
- Discrete-event control of nondeterministic systems
- Logic Synthesis for Asynchronous Controllers and Interfaces
- Logic in Computer Science
- Precongruence formats for decorated trace semantics
- Automated Assumption Generation for Compositional Verification
- Computer Aided Verification
- On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
- Optimized L*-Based Assume-Guarantee Reasoning
