×

Isabelle/Circus

swMATH ID: 15208
Software Authors: Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff
Description: Isabelle/Circus: A Process Specification and Verification Environment. The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a “shallow embedding” of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and implement tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-27705-4_20
Related Software: Isabelle/HOL; ProofPower; Isabelle; Circus; Sledgehammer; Isabelle/UTP; Z; HOL; UTP2; Saoithin; Lifting; Transfer; Handel-C; AWN; AODV; Archive Formal Proofs; Isabelle/jEdit; TPTP; Coq; ML
Cited in: 12 Publications

Citations by Year