Circus
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Refinement and verification in component-based model-driven design
- A UTP semantics for \textsf{Circus}
- A formal framework for modeling and validating simulink diagrams
- CCSP
- CirCUs
- Alloy
- Lutess
- rCOS
- ArcAngel
- SCOOP
- LOTOS
- HOL-Z
- SPARK
- TCOZ
- Simulink
- StateFlow
- JACK
- Unifying theories of time with generalised reactive processes
- CZT
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- ArcAngelC
- ProofPower
- ClawZ
- Rodin
- ProB
- The safety-critical Java memory model formalised
- Unifying theories in ProofPower-Z
- csp2B
- RiskStructures: a design algebra for risk-aware machines
- Unifying theories of reactive design contracts
- Automated verification of reactive and concurrent programs by calculation
- Alcoa
- MIO Workbench
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Z/EVES
- Z
- Modelling temporal behaviour in complex systems with Timebands
- Model transformations across views
- CSP-prover
- FDR2
- Laws of mission-based programming
- Efficient symbolic computation of process expressions
- Handel-C
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- FDR3
- Safety-critical Java programs from \textsf{Circus} models
- A CSP model of Eiffel's SCOOP
- Integrating a formal method into a software engineering process with UML and Java
- PAT
- CSPsim
- Verilog
- PTSC
- Responsiveness and stable revivals
- Interactive tool support for CSP \(\parallel\) B consistency checking
- Isabelle/Circus
- ProBE
- Simulink timed models for program verification
- Semantic domains for Handel-C
- Refinement of actions in Circus
- NAT2TEST
- Viewing CSP specifications with UML-RT diagrams
- Type checking \textsf{Circus} specifications
- Building a Modal Interface Theory for Concurrency and Data
- rCOS: defining meanings of component-based software architectures
- Unifying theories of programming in Isabelle
- HOL-TestGen
- Towards a UTP semantics for Modelica
- A two-way path between formal and informal design of embedded systems
- A stepwise approach to linking theories
- Connectors as designs
- Proving Quicksort Correct in Event-B
- Automating refinement of Circus programs
- Jaza
- Behavioural models for FMI co-simulations
- Unifying heterogeneous state-spaces with lenses
- Isabelle/UTP
- RailCNL
- ZRC
- UTPCalc
- Hume
- Circus Time with Reactive Designs
- Encoding Circus programs in ProofPower-Z
- CSP with Hierarchical State
- JCSP
- Mechanised support for sound refinement tactics
- Experiments in program verification using Event-B
- Connectors as designs: modeling, refinement and test case generation
- Mechanical reasoning about families of UTP theories
- Refinement-oriented models of Stateflow charts
- Simpl
- scientific article; zbMATH DE number 2080001 (Why is no real title available?)
- A Hoare logic for linear systems
- scientific article; zbMATH DE number 2090152 (Why is no real title available?)
- Test selection for traces refinement
- Building Specifications in the Event-B Institution
- A Unary Semigroup Trace Algebra
- Stateflow diagrams in Circus
- Mechanical Reasoning about Families of UTP Theories
- A denotational semantics for Handel-C
- A tactic language for refinement of state-rich concurrent specifications
This page was built for software: Circus
