KeY es una herramienta de verificación formal para programas Java. Acepta especificaciones escritas en el Java Modeling Language para archivos fuente de Java. Estas se transforman en teoremas de lógica dinámica y luego se comparan con la semántica del programa que también se define en términos de lógica dinámica. KeY es significativamente poderoso en que admite tanto pruebas de corrección interactivas como totalmente automatizadas. Los intentos de prueba fallidos se pueden usar para una depuración o pruebas basadas en verificación más eficientes. Ha habido varias extensiones a KeY para aplicarlo a la verificación de programas C o sistemas híbridos. KeY es desarrollado conjuntamente por el Karlsruhe Institute of Technology, Alemania; Technische Universität Darmstadt, Alemania; y Chalmers University of Technology en Gotemburgo, Suecia, y tiene licencia GPL.
- Website
- https://www.key-project.org/
