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 all top 5 Cited by 13 Authors 7 Woodcock, James C. P. 5 Foster, Simon 3 Bourke, Timothy 3 Cavalcanti, Ana 3 Höfner, Peter 3 van Glabbeek, Robert Jan 3 Zeyda, Frank 2 Wei, Kun 1 Burns, Alan D. 1 Butterfield, Andrew 1 Freitas, Leo 1 Mota, Alexandre C. 1 Thiele, Bernhard Cited in 2 Serials 1 Journal of Automated Reasoning 1 Formal Methods in System Design Cited in 3 Fields 12 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 1 Systems theory; control (93-XX) Citations by Year