Isabelle/UTP: a mechanised theory engineering framework
From MaRDI portal
Recommendations
Cites work
- A UTP semantics for \textsf{Circus}
- Automated Deduction – CADE-20
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Automatic proof and disproof in Isabelle/HOL
- Formalising foundations of mathematics
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- scientific article; zbMATH DE number 42431 (Why is no real title available?)
- scientific article; zbMATH DE number 2080001 (Why is no real title available?)
- scientific article; zbMATH DE number 1759984 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mechanical Reasoning about Families of UTP Theories
- Normal design algebra
- Saoithín: a theorem prover for UTP
- The logic of \(U\cdot(TP)^{2}\)
- The safety-critical Java memory model formalised
- Unifying theories in Isabelle/HOL
- Unifying Theories in ProofPower-Z
- Unifying theories of programming in Isabelle
- UTP semantics for Handel-C
Cited in
(28)- Designing a semantic model for a wide-spectrum language with concurrency
- Towards verification of cyber-physical systems with UTP and Isabelle/HOL
- Angelic processes for CSP via the UTP
- Unifying theories of reactive design contracts
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Unifying theories of programming in Isabelle
- Towards a UTP semantics for Modelica
- A stepwise approach to linking theories
- An Axiomatic Value Model for Isabelle/UTP
- UTPCalc -- a calculator for UTP predicates
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Saoithín: a theorem prover for UTP
- Unifying theories in Isabelle/HOL
- Behavioural models for FMI co-simulations
- Unifying heterogeneous state-spaces with lenses
- Isabelle/UTP
- The logic of \(U\cdot(TP)^{2}\)
- Mechanical reasoning about families of UTP theories
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- A Unary Semigroup Trace Algebra
- Mechanical Reasoning about Families of UTP Theories
- Mechanising a Unifying Theory
- Compositional assume-guarantee reasoning of control law diagrams using UTP
- Translation of CCS into CSP, correct up to strong bisimulation
- UTP, \textsf{\textit{Circus}}, and Isabelle
- A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming
- Towards a model-checker for \textit{\textsf{Circus}}
- APML: an architecture proof modeling language
This page was built for publication: Isabelle/UTP: a mechanised theory engineering framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2814613)
