KeY

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

Showing results 1 to 20 of 47.
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. 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
  3. De Gouw, Stijn; De Boer, Frank; Rot, Jurriaan: Proof pearl: The KeY to correct and stable sorting (2014)
  4. Kohlhase, Michael; Mance, Felix; Rabe, Florian: A universal machine for biform theory graphs (2013)
  5. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  6. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  7. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
  8. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  9. Cabot, Jordi; Pau, Raquel; Raventós, Ruth: From UML/OCL to SBVR specifications: a challenging transformation (2010) ioport
  10. 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
  11. Kauer, Stefan; Winkler, Jürgen F.H.: Mechanical inference of invariants for FOR-loops (2010)
  12. Brucker, Achim D.; Wolff, Burkhart: Semantics, calculi, and analysis for object-oriented specifications (2009)
  13. 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
  14. Feinerer, Ingo; Salzer, Gernot: A comparison of tools for teaching formal software verification (2009)
  15. Gladisch, Christoph: Could we have chosen a better loop invariant or method contract? (2009)
  16. Roldán, Manuel; Durán, Francisco; Vallecillo, Antonio: Invariant-driven specifications in Maude (2009)
  17. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)
  18. Costal, Dolors; Gómez, Cristina; Queralt, Anna; Raventós, Ruth; Teniente, Ernest: Improving the definition of general constraints in UML (2008) ioport
  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) ioport

1 2 3 next


Further publications can be found at: http://www.key-project.org/publicat.html