Cited in
(only showing first 100 items - show all)- Semantic domains for Handel-C
- Unifying theories of programming in Isabelle
- Test selection for traces refinement
- The behavioural semantics of Event-B refinement
- TraitCbC
- rCOS: a refinement calculus of object systems
- Testing for refinement in \textsf{Circus}
- Proving Quicksort Correct in Event-B
- A process algebraic framework for specification and validation of real-time systems
- A formal framework for modeling and validating simulink diagrams
- CSP with Hierarchical State
- Building Specifications in the Event-B Institution
- Safety-critical Java programs from \textsf{Circus} models
- The safety-critical Java memory model formalised
- Unifying theories in ProofPower-Z
- Type checking \textsf{Circus} specifications
- A timeband framework for modelling real-time systems
- SafeJML
- Unifying theories of time with generalised reactive processes
- Viewing CSP specifications with UML-RT diagrams
- Automated verification of reactive and concurrent programs by calculation
- Towards a UTP semantics for Modelica
- Unifying heterogeneous state-spaces with lenses
- Mechanical Reasoning about Families of UTP Theories
- RiskStructures: a design algebra for risk-aware machines
- scientific article; zbMATH DE number 2080001 (Why is no real title available?)
- Testing using CSP Models: Time, Inputs, and Outputs
- Laws of mission-based programming
- A CSP model of Eiffel's SCOOP
- Building a Modal Interface Theory for Concurrency and Data
- Stateflow diagrams in Circus
- Responsiveness and stable revivals
- A denotational semantics for Handel-C
- A semantics for behavior trees using CSP with specification commands
- A Unary Semigroup Trace Algebra
- rCOS: defining meanings of component-based software architectures
- Cameo: an alternative model of concurrency for Eiffel
- Interface theories for concurrency and data
- Angelic nondeterminism in the unifying theories of programming
- Unifying theories of reactive design contracts
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- scientific article; zbMATH DE number 2090152 (Why is no real title available?)
- Experiments in program verification using Event-B
- Mechanised support for sound refinement tactics
- Connectors as designs: modeling, refinement and test case generation
- Mechanical reasoning about families of UTP theories
- Refinement-oriented models of Stateflow charts
- A two-way path between formal and informal design of embedded systems
- Circus Time with Reactive Designs
- Refinement and verification in component-based model-driven design
- From control law diagrams to Ada via \textsf{Circus}
- Modelling temporal behaviour in complex systems with Timebands
- A refinement strategy for Circus
- Building program construction and verification tools from algebraic principles
- FM 2005: Formal Methods
- Simulink timed models for program verification
- A UTP semantics for \textsf{Circus}
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- On integrating confidentiality and functionality in a formal method
- Refinement patterns for ASTDs
- Behavioural models for FMI co-simulations
- Refinement of actions in Circus
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- CCSP
- CirCUs
- Alloy
- Lutess
- rCOS
- ArcAngel
- SCOOP
- LOTOS
- HOL-Z
- SPARK
- TCOZ
- Simulink
- JACK
- StateFlow
- CZT
- ArcAngelC
- ClawZ
- ProofPower
- ProB
- Rodin
- csp2B
- Alcoa
- MIO Workbench
- Z/EVES
- Z
- CSP-prover
- FDR2
- Handel-C
- FDR3
- CSPsim
- PAT
- PTSC
- Verilog
- Isabelle/Circus
- ProBE
- NAT2TEST
This page was built for software: Circus
