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