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

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

1 2 3 4 next

  1. de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic: Verifying OpenJDK’s sort method for generic collections (2019)
  2. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  3. Platzer, André: Uniform substitution at one Fell swoop (2019)
  4. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  5. Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
  6. 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)
  7. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  8. Fulton, Nathan; Mitsch, Stefan; Quesel, Jan-David; Völp, Marcus; Platzer, André: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems (2015)
  9. Montenegro, Manuel; Peña, Ricardo; Sánchez-Hernández, Jaime: A generic intermediate representation for verification condition generation (2015)
  10. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  11. 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
  12. De Gouw, Stijn; De Boer, Frank; Rot, Jurriaan: Proof pearl: The KeY to correct and stable sorting (2014)
  13. Kohlhase, Michael; Mance, Felix; Rabe, Florian: A universal machine for biform theory graphs (2013)
  14. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  15. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  16. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
  17. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  18. Cabot, Jordi; Pau, Raquel; Raventós, Ruth: From UML/OCL to SBVR specifications: a challenging transformation (2010) ioport
  19. 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
  20. Kauer, Stefan; Winkler, Jürgen F. H.: Mechanical inference of invariants for FOR-loops (2010)

1 2 3 4 next

Further publications can be found at: