Automated verification of reactive and concurrent programs by calculation
From MaRDI portal
Publication:2043817
DOI10.1016/j.jlamp.2021.100681OpenAlexW3046818083MaRDI QIDQ2043817
Ana Cavalcanti, Kangfeng Ye, Simon Foster, J. C. P. Woodcock
Publication date: 3 August 2021
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2007.13529
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Generalised rely-guarantee concurrency: an algebraic foundation
- From control law diagrams to Ada via \textsf{Circus}
- Normal design algebra
- A process algebraic framework for specification and validation of real-time systems
- A UTP semantics for \textsf{Circus}
- Fixed point theorems and semantics: A folk tale
- Calculational verification of reactive programs with reactive relations and Kleene algebra
- Unifying theories of time with generalised reactive processes
- Taming Dr. Frankenstein: contract-based design for cyber-physical systems
- Unifying theories of reactive design contracts
- Modal Kleene algebra applied to program correctness
- A lattice-theoretical fixpoint theorem and its applications
- Unifying Heterogeneous State-Spaces with Lenses
- Component Publications and Compositions
- Multiple Viewpoint Contract-Based Specification and Design
- Quantales and Temporal Logics
- A Theory of Communicating Sequential Processes
- Laws of programming
- Guarded commands, nondeterminacy and formal derivation of programs
- Refinement Calculus
- Formal Verification of Simulink/Stateflow Diagrams
- Object-Orientation in the UTP
- FM 2005: Formal Methods
This page was built for publication: Automated verification of reactive and concurrent programs by calculation
