Refinement in Circus

DOI10.1007/3-540-45614-7_26MaRDI QIDQ4808845zbMATH OpenFDO

Authors Augusto Sampaio, Ana Cavalcanti, Jim Woodcock

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2391/23910451.htm

zbMATH Keywords

CSPdistributionunifying theories of programmingZ

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Refinement of actions in Circus
• A refinement strategy for Circus
• Unifying concurrent and relational refinement
• The semantics of Circus
• A tactic language for refinement of state-rich concurrent specifications

Cited in

(13)

• Refinement of actions in Circus
• Building a Modal Interface Theory for Concurrency and Data
• Unifying theories of programming in Isabelle
• Proving Quicksort Correct in Event-B
• Automating refinement of Circus programs
• Experiments in program verification using Event-B
• The semantics of Circus
• A tactic language for refinement of state-rich concurrent specifications
• Interface theories for concurrency and data
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Formal verification of BDI agents
• A refinement strategy for Circus
• Isabelle/Circus

Describes a project that uses

Uses Software

• Circus

This page was built for publication: Refinement in Circus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4808845)