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 39 articles )

Showing results 1 to 20 of 39.
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 \textsfCircus (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. Amálio, Nuno; Polack, Fiona; Stepney, Susan: Frameworks based on templates for rigorous model-driven development (2007) ioport
  18. Borges, Rafael Magalhães; Mota, Alexandre Cabral: Integrating UML and formal methods (2007) ioport
  19. Derrick, John; Wehrheim, Heike: On using data abstractions for model checking refinements (2007)
  20. Freitas, Leo; Woodcock, Jim: Proving theorems about JML classes (2007)

1 2 next