ProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. The DAZ tool supporting refinement of Z to the SPARK subset of Ada is also available.

References in zbMATH (referenced in 35 articles )

Showing results 1 to 20 of 35.
Sorted by year (citations)

1 2 next

  1. da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila: Theorem proving graph grammars with attributes and negative application conditions (2017)
  2. Gilbert, Frédéric: Proof certificates in PVS (2017)
  3. Zeyda, Frank; Foster, Simon; Freitas, Leo: An axiomatic value model for Isabelle/UTP (2017)
  4. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  5. Arthan, Rob: On definitions of constants and types in HOL (2016)
  6. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  7. Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
  8. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  9. Zhu, H.; He, Jifeng; Qin, Shengchao; Brooke, Phillip: Denotational semantics and its algebraic derivation for an event-driven system-level language (2015)
  10. Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim: Test-data generation for control coverage by proof (2014)
  11. Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-based verification of implementations of Stateflow charts (2014) ioport
  12. Butterfield, Andrew: The logic of $U\cdot(TP)^2$ (2013)
  13. Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim: Simulink timed models for program verification (2013)
  14. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  15. Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: Unifying theories in ProofPower-Z (2013)
  16. Wei, Kun; Woodcock, Jim; Burns, Alan: Modelling temporal behaviour in complex systems with Timebands (2013)
  17. Zeyda, Frank; Cavalcanti, Ana: Higher-order UTP for a theory of methods (2013)
  18. Kumar, Ramana; Hurd, Joe: Standalone tactics using OpenTheory (2012)
  19. Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-oriented models of Stateflow charts (2012)
  20. Zeyda, Frank; Cavalcanti, Ana: Mechanical reasoning about families of UTP theories (2012)

1 2 next

Further publications can be found at: