ProofPower

swMATH6339MaRDI QIDQ18467FDOQ18467

Author name not available (Why is that?)

Cited In (51)

• Building a library of mechanized mathematical proofs: Why do it? And what is it like to do?
• Now \(f\) is continuous (exercise!)
• 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
• Witnessing (co)datatypes
• 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
• Higher-order UTP for a theory of methods
• Mechanised support for sound refinement tactics
• Mechanical reasoning about families of UTP theories
• Refinement-oriented models of Stateflow charts
• Conversion of HOL Light proofs into Metamath
• A verified proof checker for higher-order logic
• Modelling temporal behaviour in complex systems with Timebands
• 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
• Theorem proving graph grammars with attributes and negative application conditions
• Title not available (Why is that?)
• 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
• Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
• Rewriting conversions implemented with continuations
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• HOL Zero's solutions for Pollack-inconsistency
• Encoding Circus programs in ProofPower-Z
• Automating refinement of Circus programs
• FM 2005: Formal Methods
• Standalone Tactics Using OpenTheory
• Using formal reasoning on a model of tasks for FreeRTOS
• A tactic language for refinement of state-rich concurrent specifications
• 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
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• 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
• Mechanical Reasoning about Families of UTP Theories
• A consistent foundation for Isabelle/HOL
• A consistent foundation for Isabelle/HOL

This page was built for software: ProofPower