A UTP semantics for \textsf{Circus}
From MaRDI portal
Publication:1019016
Recommendations
Cites work
- A refinement strategy for Circus
- A theoretical basis for stepwise refinement and the programming calculus
- FM 2005: Formal Methods
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 605806 (Why is no real title available?)
- scientific article; zbMATH DE number 605917 (Why is no real title available?)
- scientific article; zbMATH DE number 2013582 (Why is no real title available?)
- scientific article; zbMATH DE number 2080001 (Why is no real title available?)
- scientific article; zbMATH DE number 1487746 (Why is no real title available?)
- scientific article; zbMATH DE number 2172805 (Why is no real title available?)
- Mechanising a Unifying Theory
- Unifying Theories in ProofPower-Z
- ZRC -- A refinement calculus for Z
Cited in
(46)- Unifying theories of time with generalised reactive processes
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- The safety-critical Java memory model formalised
- RiskStructures: a design algebra for risk-aware machines
- Unifying theories of reactive design contracts
- Automated verification of reactive and concurrent programs by calculation
- Reasoning about iteration and recursion uniformly based on big-step semantics
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Modelling temporal behaviour in complex systems with Timebands
- Model transformations across views
- Laws of mission-based programming
- Safety-critical Java programs from \textsf{Circus} models
- Isabelle/UTP: a mechanised theory engineering framework
- Towards Algebraic Semantics of Circus Time
- Simulink timed models for program verification
- Type checking \textsf{Circus} specifications
- Unifying theories of programming in Isabelle
- A stepwise approach to linking theories
- An Axiomatic Value Model for Isabelle/UTP
- Specification coverage for testing in Circus
- Behavioural models for FMI co-simulations
- Unifying heterogeneous state-spaces with lenses
- Circus Time with Reactive Designs
- The logic of \(U\cdot(TP)^{2}\)
- A note on traces refinement and the conf relation in the unifying theories of programming
- UTP semantics for Handel-C
- Encoding Circus programs in ProofPower-Z
- Mechanised support for sound refinement tactics
- Mechanical reasoning about families of UTP theories
- scientific article; zbMATH DE number 2080001 (Why is no real title available?)
- Test selection for traces refinement
- Building Specifications in the Event-B Institution
- A tactic language for refinement of state-rich concurrent specifications
- FM 2005: Formal Methods
- Information Flow Control-by-Construction for an Object-Oriented Language
- Flexible Correct-by-Construction Programming
- From control law diagrams to Ada via \textsf{Circus}
- UTP, \textsf{\textit{Circus}}, and Isabelle
- Towards a model-checker for \textit{\textsf{Circus}}
- Formal verification of BDI agents
- Optics
- On integrating confidentiality and functionality in a formal method
- Testing for refinement in \textsf{Circus}
- Categorical foundations for structured specifications in \(\mathsf{Z}\)
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- A timeband framework for modelling real-time systems
This page was built for publication: A UTP semantics for \textsf{Circus}
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1019016)
