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 53 articles , 3 standard articles )

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

1 2 3 next

  1. Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
  2. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  3. Montenegro, Manuel; Peña, Ricardo; Sánchez-Hernández, Jaime: A generic intermediate representation for verification condition generation (2015)
  4. Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter; Ulbrich, Mattias: The key platform for verification and analysis of Java programs (2014) ioport
  5. De Gouw, Stijn; De Boer, Frank; Rot, Jurriaan: Proof pearl: The KeY to correct and stable sorting (2014)
  6. Kohlhase, Michael; Mance, Felix; Rabe, Florian: A universal machine for biform theory graphs (2013)
  7. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  8. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  9. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
  10. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  11. Cabot, Jordi; Pau, Raquel; Raventós, Ruth: From UML/OCL to SBVR specifications: a challenging transformation (2010) ioport
  12. 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) ioport
  13. Kauer, Stefan; Winkler, Jürgen F.H.: Mechanical inference of invariants for FOR-loops (2010)
  14. Brucker, Achim D.; Wolff, Burkhart: Semantics, calculi, and analysis for object-oriented specifications (2009)
  15. 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) ioport
  16. Feinerer, Ingo; Salzer, Gernot: A comparison of tools for teaching formal software verification (2009)
  17. Gladisch, Christoph: Could we have chosen a better loop invariant or method contract? (2009)
  18. Roldán, Manuel; Durán, Francisco; Vallecillo, Antonio: Invariant-driven specifications in Maude (2009)
  19. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)
  20. Costal, Dolors; Gómez, Cristina; Queralt, Anna; Raventós, Ruth; Teniente, Ernest: Improving the definition of general constraints in UML (2008) ioport

1 2 3 next

Further publications can be found at: