Angelic processes for CSP via the UTP
From MaRDI portal
Publication:1757156
DOI10.1016/j.tcs.2018.10.008zbMath1410.68236OpenAlexW2896734676MaRDI QIDQ1757156
Publication date: 2 January 2019
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://eprints.whiterose.ac.uk/137382/1/TCS2018.pdf
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A theoretical basis for stepwise refinement and the programming calculus
- ArcAngel: a tactic language for refinement
- Angelic nondeterminism in the unifying theories of programming
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- Data refinement by calculation
- Data refinement of predicate transformers
- LR-parsing derived
- A UTP approach for rTiMo
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- A tactic calculus. --- Abridged version
- Understanding concurrent systems
- Isabelle/UTP: A Mechanised Theory Engineering Framework
- Simulink Timed Models for Program Verification
- UTP Designs for Binary Multirelations
- Unifying Theories in Isabelle/HOL
- The Logic of U ·(TP)2
- A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes
- The Miracle of Reactive Programming
- Encoding Circus Programs in ProofPowerZ
- Guarded commands, nondeterminacy and formal derivation of programs
- Refinement Calculus
- A Theory of Pointers for the UTP
- Nondeterministic Algorithms
- The complexity of theorem-proving procedures
- On context-free languages and push-down automata
- Integrated Formal Methods
This page was built for publication: Angelic processes for CSP via the UTP