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