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