KeY (logiciel)

Pour les articles homonymes, voir Key.

Cet article est une ébauche concernant un logiciel et l’informatique théorique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Le logiciel KeY est un outil de vérification formelle de programmes Java^[1]. Débuté en 1998, le projet KeY est porté par l'Institut de technologie de Karlsruhe, l'Université de technologie de Darmstadt et l'École polytechnique Chalmers^[2]. KeY accepte les spécifications écrites à l'aide du Java Modeling Language (JML).

Notes et références

↑ (en) Bernhard Beckert, Reiner Hähnle et Peter H. Schmitt, Verification of Object-oriented Software : The KeY Approach, Springer-Verlag, 2007, 658 p. (ISBN 978-3-540-68977-5 et 3-540-68977-X, lire en ligne)
↑ (en) « KeY Project: Integrated Deductive Software Design », sur ira.uka.de, 27 février 2017 (consulté le 29 février 2020).