ProofPower

swMATH6339MaRDI QIDQ18467FDOQ18467

Author name not available (Why is that?)

Cited In (52)

• Building a Library of Mechanized Mathematical Proofs: Why Do It? and What Is It Like to Do?
• 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
• The Logic of U ·(TP)2
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• A Consistent Foundation for Isabelle/HOL
• Unifying Heterogeneous State-Spaces with Lenses
• 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
• 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
• 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
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• An Axiomatic Value Model for Isabelle/UTP
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• Witnessing (Co)datatypes
• HOL Zero’s Solutions for Pollack-Inconsistency
• 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
• FM 2005: Formal Methods
• Simulink Timed Models for Program Verification
• Standalone Tactics Using OpenTheory
• Using formal reasoning on a model of tasks for FreeRTOS
• A tactic language for refinement of state-rich concurrent specifications
• Higher-Order UTP for a Theory of Methods
• Unifying Theories in Isabelle/HOL
• Formalization of the fundamental group in untyped set theory using auto2
• 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
• Now f is continuous (exercise
• 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
• Automating Refinement of Circus Programs
• A timeband framework for modelling real-time systems
• Unifying Theories of Programming in Isabelle
• Automating Event-B invariant proofs by rippling and proof patching
• Encoding Circus Programs in ProofPowerZ
• Mechanical Reasoning about Families of UTP Theories
• A consistent foundation for Isabelle/HOL

This page was built for software: ProofPower