Z/EVES

Z/EVES Eclipse prover IDE. Community Z Tools provide an Eclipse-based IDE and integration with Z/EVES theorem prover. This extends the development of Z specifications in CZT with theorem proving and verification capabilities. Z/EVES Eclipse provides a modern environment to use the Z/EVES theorem prover. It is an alternative to the original Z/EVES UI, which is no longer in development and has issues when used with modern operating systems. Z/EVES Eclipse brings the Z/EVES theorem prover to a modern IDE and supports all Z/EVES functionality: writing and sending proof commands to the prover, viewing proof output, querying lemmas, section management, etc.


References in zbMATH (referenced in 37 articles )

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

1 2 next

  1. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  2. Freitas, Leo; Watson, Paul: Formalizing workflows partitioning over federated clouds: multi-level security and costs (2014)
  3. Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: Unifying theories in ProofPower-Z (2013)
  4. Shin, Dongsoo: Conics on a general hypersurface in complex projective spaces (2013)
  5. Woodcock, Jim; Bandur, Victor: Unifying theories of undefinedness in UTP (2013)
  6. da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Souza Neto, Plácido A.: JCML: A specification language for the runtime verification of Java card programs (2012)
  7. Derrick, John; North, Siobhán; Simons, Anthony J.H.: Z2SAL: a translation-based model checker for Z (2011)
  8. Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana: A tactic language for refinement of state-rich concurrent specifications (2011)
  9. Butterfield, Andrew; Freitas, Leo; Woodcock, Jim: Mechanising a formal model of flash memory (2009)
  10. Freitas, Leo; Woodcock, Jim; Fu, Zheng: POSIX file store in Z/Eves: An experiment in the verified software repository (2009)
  11. Freitas, Leo; Woodcock, Jim; Zhang, Yichi: Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository (2009)
  12. Mammar, Amel: A systematic approach to generate B preconditions: application to the database domain (2009) ioport
  13. Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: A UTP semantics for \ssfCircus (2009)
  14. Freitas, Leo; Woodcock, Jim: Mechanising mondex with z/Eves (2008) ioport
  15. George, Chris; Haxthausen, Anne E.: Specification, proof, and model checking of the mondex electronic purse using RAISE (2008) ioport
  16. Haneberg, Dominik; Schellhorn, Gerhard; Grandy, Holger; Reif, Wolfgang: Verification of mondex electronic purses with KIV: from transactions to a security protocol (2008) ioport
  17. Derrick, John; Wehrheim, Heike: On using data abstractions for model checking refinements (2007)
  18. Freitas, Leo; Woodcock, Jim: Proving theorems about JML classes (2007)
  19. Bicarregui, J.C.; Hoare, C.A.R.; Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler (2006)
  20. Freitas, Leo; Woodcock, Jim; Cavalcanti, Ana: State-rich model checking (2006) ioport

1 2 next