Cited in
(92)- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- Mechanical Reasoning about Families of UTP Theories
- Now \(f\) is continuous (exercise!)
- Modelling temporal behaviour in complex systems with Timebands
- scientific article; zbMATH DE number 2079997 (Why is no real title available?)
- Witnessing (co)datatypes
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Rewriting conversions implemented with continuations
- Conversion of HOL Light proofs into Metamath
- Theorem proving graph grammars with attributes and negative application conditions
- Higher-order UTP for a theory of methods
- Building a library of mechanized mathematical proofs: Why do it? And what is it like to do?
- Standalone Tactics Using OpenTheory
- QED reloaded: towards a pluralistic formal library of mathematical knowledge
- An Axiomatic Value Model for Isabelle/UTP
- Formalization of real analysis: a survey of proof assistants and libraries
- Unifying theories of programming in Isabelle
- Unifying theories in ProofPower-Z
- FM 2005: Formal Methods
- A consistent foundation for Isabelle/HOL
- A consistent foundation for Isabelle/HOL
- A UTP semantics for \textsf{Circus}
- Mechanised support for sound refinement tactics
- A timeband framework for modelling real-time systems
- Mechanical reasoning about families of UTP theories
- Refinement-oriented models of Stateflow charts
- On definitions of constants and types in HOL
- Unifying theories of programming. Second international symposium, UTP 2008, Dublin, Ireland, September 8--10, 2008. Revised selected papers
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- Proof certificates in PVS
- A process algebraic framework for specification and validation of real-time systems
- Using formal reasoning on a model of tasks for FreeRTOS
- A tactic language for refinement of state-rich concurrent specifications
- Test-data generation for control coverage by proof
- Automating Event-B invariant proofs by rippling and proof patching
- Prosper
- ArcAngel
- RAISE
- TCOZ
- JACK
- StateFlow
- CZT
- ArcAngelC
- ClawZ
- Saoithin
- UTP2
- Alcoa
- Milawa
- Z/EVES
- Z
- Handel-C
- Jitawa
- ModuRes
- FreeRTOS
- PTSC
- Verilog
- Isabelle/Circus
- ProBE
- HOL Zero
- HOL-TestGen
- Mechanising a Unifying Theory
- Unifying Theories in ProofPower-Z
- Isabelle/UTP
- Circus
- Hume
- IsarMathLib
- ZRC
- UTPCalc
- AGREE
- GitLab
- JCSP
- NASA PVS
- EVES
- XIsabelle
- Cambridge LCF
- Jape
- OpenTheory
- From control law diagrams to Ada via \textsf{Circus}
- Angelic processes for CSP via the UTP
- Metamath Zero
- Unifying theories in Isabelle/HOL
- A verified proof checker for higher-order logic
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- Unifying heterogeneous state-spaces with lenses
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- HOL Zero's solutions for Pollack-inconsistency
- scientific article; zbMATH DE number 1863376 (Why is no real title available?)
- The logic of \(U\cdot(TP)^{2}\)
- Encoding Circus programs in ProofPower-Z
- Automating refinement of Circus programs
- Simulink timed models for program verification
This page was built for software: ProofPower
