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