The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of Karlsruhe Institute of Technology and Chalmers University of Technology, Gothenburg and TU Darmstadt.

References in zbMATH (referenced in 49 articles )

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

1 2 3 next

  1. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  2. De Gouw, Stijn; De Boer, Frank; Rot, Jurriaan: Proof pearl: The KeY to correct and stable sorting (2014)
  3. Kohlhase, Michael; Mance, Felix; Rabe, Florian: A universal machine for biform theory graphs (2013)
  4. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  5. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  6. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for alloy specifications (2012)
  7. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  8. Cabot, Jordi; Pau, Raquel; Raventós, Ruth: From UML/OCL to SBVR specifications: a challenging transformation (2010)
  9. du Bousquet, Lydie; Ledru, Yves; Maury, Olivier; Oriat, Catherine; Lanet, Jean-Louis: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies (2010)
  10. Kauer, Stefan; Winkler, Jürgen F.H.: Mechanical inference of invariants for FOR-loops (2010)
  11. Brucker, Achim D.; Wolff, Burkhart: Semantics, calculi, and analysis for object-oriented specifications (2009)
  12. du Bousquet, Lydie; Nakamura, Masahide; Yan, Ben; Igaki, Hiroshi: Using formal methods to increase confidence in a home network system implementation: a case study (2009)
  13. Feinerer, Ingo; Salzer, Gernot: A comparison of tools for teaching formal software verification (2009)
  14. Gladisch, Christoph: Could we have chosen a better loop invariant or method contract? (2009)
  15. Roldán, Manuel; Durán, Francisco; Vallecillo, Antonio: Invariant-driven specifications in Maude (2009)
  16. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)
  17. Bubel, Richard; Roth, Andreas; Rümmer, Philipp: Ensuring the correctness of lightweight tactics for javacard dynamic logic. (2008)
  18. Costal, Dolors; Gómez, Cristina; Queralt, Anna; Raventós, Ruth; Teniente, Ernest: Improving the definition of general constraints in UML (2008)
  19. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura: Valigator: A verification tool with bound and invariant generation (2008)
  20. Marković, Slaviša; Baar, Thomas: Refactoring OCL annotated UML class diagrams (2008)

1 2 3 next

Further publications can be found at: