From 9ec556aa596056af0f4f5e20528cdf1508232bd5 Mon Sep 17 00:00:00 2001 From: pron Date: Mon, 18 Jan 2016 14:46:11 +0200 Subject: [PATCH] Add Krakatoa --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 6680e74..13b114b 100644 --- a/README.md +++ b/README.md @@ -279,6 +279,7 @@ A curated list of awesome Java frameworks, libraries and software. * [jCUTE](https://github.com/osl/jcute) - Concolic unit testing engine that automatically generates unit tests. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving. * [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Detects nonconformances between code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected. * [KeY](http://key-project.org/) - 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. Uses JML for specification and symbolic execution for verification. +* [Krakatoa](http://krakatoa.lri.fr/) - Krakatoa is a front-end of the [Why](http://why.lri.fr/) platform for deductive program verification. Krakatoa deals with Java programs annotated in a variant of the The Java Modeling Language (JML). * [OpenJML](http://openjml.github.io/) - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers. ## Functional Programming