ProofPower
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.
Keywords for this software
References in zbMATH (referenced in 31 articles )
Showing results 1 to 20 of 31.
Sorted by year (- Arthan, Rob: On definitions of constants and types in HOL (2016)
- Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
- Zhu, H.; He, Jifeng; Qin, Shengchao; Brooke, Phillip: Denotational semantics and its algebraic derivation for an event-driven system-level language (2015)
- Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim: Test-data generation for control coverage by proof (2014)
- Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-based verification of implementations of Stateflow charts (2014)
- Butterfield, Andrew: The logic of $U\cdot(TP)^2$ (2013)
- Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim: Simulink timed models for program verification (2013)
- Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: Unifying theories in ProofPower-Z (2013)
- Wei, Kun; Woodcock, Jim; Burns, Alan: Modelling temporal behaviour in complex systems with Timebands (2013)
- Zeyda, Frank; Cavalcanti, Ana: Higher-order UTP for a theory of methods (2013)
- Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-oriented models of Stateflow charts (2012)
- Zeyda, Frank; Cavalcanti, Ana: Mechanical reasoning about families of UTP theories (2012)
- Zeyda, Frank; Oliveira, Marcel; Cavalcanti, Ana: Mechanised support for sound refinement tactics (2012)
- Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana: A tactic language for refinement of state-rich concurrent specifications (2011)
- Zeyda, Frank; Cavalcanti, Ana: Automating refinement of Circus programs (2011)
- Arthan, R.D.: Building a library of mechanized mathematical proofs: Why do it? And what is it like to do? (2010)
- Butterfield, Andrew (ed.): Unifying theories of programming. Second international symposium, UTP 2008, Dublin, Ireland, September 8--10, 2008. Revised selected papers (2010)
- Zeyda, Frank; Cavalcanti, Ana: Encoding Circus programs in ProofPower-Z (2010)
- Boulton, Richard; Hurd, Joe; Slind, Konrad: Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (2009)
- Norrish, Michael: Rewriting conversions implemented with continuations (2009)
Further publications can be found at: http://www.lemma-one.com/ProofPower/papers/papers.html