Specification and verification of concurrent systems by causality and realizability
From MaRDI portal
Publication:6049931
DOI10.1016/j.tcs.2023.114106OpenAlexW4385478533MaRDI QIDQ6049931
Publication date: 18 September 2023
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2023.114106
Cites Work
- A theory for nondeterminism, parallelism, communication, and concurrency
- Recognizing safety and liveness
- An extensional fixed-point semantics for nondeterministic data flow
- Power domains
- A fully abstract trace model for dataflow and asynchronous networks
- Duration calculus. A formal approach to real-time systems.
- Isabelle/HOL. A proof assistant for higher-order logic
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts
- Computability and realizability for interactive computations
- Verifying of interface assertions for infinite state Mealy machines
- Concurrency in synchronous systems
- Specification and Development of Interactive Systems
- On Fixed Points of Strictly Causal Functions
- Automata Studies. (AM-34)
- The Orc Programming Language
- A fixpoint semantics for nondeterministic data flow
- A Powerdomain Construction
- Soundness and Completeness of an Axiom System for Program Verification
- Reo: a channel-based coordination model for component composition
- Elements of Stream Calculus
- A Generalized Modality for Recursion
- A Functional Calculus for Specification and Verification of Nondeterministic Interactive Systems
- Recursive Predicates and Quantifiers
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Specification and verification of concurrent systems by causality and realizability
