Isabelle/UTP
From MaRDI portal
Cited in
(47)- Designing a semantic model for a wide-spectrum language with concurrency
- Angelic processes for CSP via the UTP
- HOL-OCL
- ProofPower
- Saoithin
- UTP2
- PROMELA
- RiskStructures: a design algebra for risk-aware machines
- Unifying theories of reactive design contracts
- Automated verification of reactive and concurrent programs by calculation
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Z
- Handel-C
- FDR3
- pGCL
- ModuRes
- Verilog
- Automated reasoning for probabilistic sequential programs with theorem proving
- Isabelle/Circus
- HOL-TestGen
- 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
- Behavioural models for FMI co-simulations
- Unifying heterogeneous state-spaces with lenses
- RailCNL
- ZRC
- Circus
- UTPCalc
- JCSP
- Ordinary Differential Equations
- Isabelle/DOF
- Binary Multirelations
- Algebraic_VCs
- Differential_Game_Logic
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- A Unary Semigroup Trace Algebra
- OCRA
- Transformer semantics
- Program Construction and Verification Components Based on Kleene Algebra
- Transformer Semantics
- Differential Game Logic
- Binary Multirelations
- Ordinary Differential Equations
This page was built for software: Isabelle/UTP