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

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

1 2 3 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  2. Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
  3. Cristiá, Maximiliano; Rossi, Gianfranco: A decision procedure for sets, binary relations and partial functions (2016)
  4. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  5. Freitas, Leo; Watson, Paul: Formalizing workflows partitioning over federated clouds: multi-level security and costs (2014)
  6. Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: Unifying theories in ProofPower-Z (2013)
  7. Shin, Dongsoo: Conics on a general hypersurface in complex projective spaces (2013)
  8. Woodcock, Jim; Bandur, Victor: Unifying theories of undefinedness in UTP (2013)
  9. 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)
  10. Derrick, John; North, Siobhán; Simons, Anthony J. H.: Z2SAL: a translation-based model checker for Z (2011)
  11. Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana: A tactic language for refinement of state-rich concurrent specifications (2011)
  12. Butterfield, Andrew; Freitas, Leo; Woodcock, Jim: Mechanising a formal model of flash memory (2009)
  13. Freitas, Leo; Woodcock, Jim; Fu, Zheng: POSIX file store in Z/Eves: An experiment in the verified software repository (2009)
  14. Freitas, Leo; Woodcock, Jim; Zhang, Yichi: Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository (2009)
  15. Mammar, Amel: A systematic approach to generate B preconditions: application to the database domain (2009) ioport
  16. Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: A UTP semantics for \textsfCircus (2009)
  17. Freitas, Leo; Woodcock, Jim: Mechanising mondex with z/Eves (2008) ioport
  18. George, Chris; Haxthausen, Anne E.: Specification, proof, and model checking of the mondex electronic purse using RAISE (2008) ioport
  19. Haneberg, Dominik; Schellhorn, Gerhard; Grandy, Holger; Reif, Wolfgang: Verification of mondex electronic purses with KIV: from transactions to a security protocol (2008) ioport
  20. Amálio, Nuno; Polack, Fiona; Stepney, Susan: Frameworks based on templates for rigorous model-driven development (2007) ioport

1 2 3 next