Compositional Reasoning
From MaRDI portal
Publication:3176370
DOI10.1007/978-3-319-10575-8_12zbMath1392.68249OpenAlexW4241926562MaRDI QIDQ3176370
Kedar S. Namjoshi, Dimitra Giannakopoulou, Corina S. Păsăreanu
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_12
Related Items
Proving the existence of fair paths in infinite-state systems, \textsc{LTL} falsification in infinite-state systems
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
- Unnamed Item
- Modular verification of multithreaded programs
- A semantics for concurrent separation logic
- 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
- Automatic symbolic compositional verification by learning assumptions
- Local proofs for global safety properties
- Learning regular sets from queries and counterexamples
- Inference of finite automata using homing sequences
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Local Symmetry and Compositional Verification
- All for the Price of Few
- Uncovering Symmetries in Irregular Process Networks
- Inductive data flow graphs
- Verification of parameterized concurrent programs by modular reasoning about data and control
- On the completeness of compositional reasoning methods
- Learning Probabilistic Systems from Tree Samples
- Compositionality Entails Sequentializability
- Learning-Based Compositional Verification for Synchronous Probabilistic Systems
- Temporal Logic and Fair Discrete Systems
- Abstraction and Abstraction Refinement
- Process Algebra and Model Checking
- Alternating-time temporal logic
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- Local Proofs for Linear-Time Properties of Concurrent Programs
- An abstract account of composition
- Learning Minimal Separating DFA’s for Compositional Verification
- Tentative steps toward a development method for interfering programs
- Proofs of Networks of Processes
- On the Construction of Submodule Specifications and Communication Protocols
- Guarded commands, nondeterminacy and formal derivation of programs
- Verifying properties of parallel programs
- Proving the Correctness of Multiprocess Programs
- Synthesis of interface specifications for Java classes
- Parallelizing a Symbolic Compositional Model-Checking Algorithm
- Predicate abstraction and refinement for verifying multi-threaded programs
- Symmetry and Completeness in the Analysis of Parameterized Systems
- Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
- Nonlinear dynamics of networks: the groupoid formalism
- An axiomatic basis for computer programming
- CONCUR 2003 - Concurrency Theory
