From 1d3f52a408903264c1b8026fd46fa72c60865f9f Mon Sep 17 00:00:00 2001 From: pron Date: Sat, 31 Oct 2015 08:35:56 +0200 Subject: [PATCH] Fixes --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 70ba5c1..5e80358 100644 --- a/README.md +++ b/README.md @@ -254,12 +254,12 @@ A curated list of awesome Java frameworks, libraries and software. *Formal-methods tools: proof assistants, model checking, symbolic execution etc.* -* [CATG](https://github.com/ksen007/janala2) - A concolic unit testing engine for Java programs. Automatically generates unit tests for Java programs using formal methods. +* [CATG](https://github.com/ksen007/janala2) - Concolic unit testing engine. Automatically generates unit tests for Java programs using formal methods. * [Checker Framework](http://types.cs.washington.edu/checker-framework/) - Pluggable type systems for Java. Includes nullness types, physical units, immutability types and more. * [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon detects likely program invariants and can generate JML specs based on those invariats. * [Java Modeling Language (JML)](http://www.jmlspecs.org) - A behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. Used by several other Java verification tools. * [Java Path Finder (JPF)](http://babelfish.arc.nasa.gov/trac/jpf) - A JVM formal verification tool containing a model checker for Java bytecode and more. Created by NASA. -* [jCUTE](https://github.com/osl/jcute) - A Java Concolic Unit Testing Engine that automatically generates unit tests for Java programs. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving. +* [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 Java 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. * [OpenJML](http://openjml.github.io/) - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.