From 168515e29917e18d852e6c6b2e00de90a296b12d Mon Sep 17 00:00:00 2001 From: pron Date: Mon, 5 Oct 2015 16:49:16 +0300 Subject: [PATCH 1/5] Added formal verification category --- README.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/README.md b/README.md index a749436..6b4f33b 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,7 @@ A curated list of awesome Java frameworks, libraries and software. - [Distributed Databases](#distributed-databases) - [Distribution](#distribution) - [Document Processing](#document-processing) + - [Formal Verification](#formal-verification) - [Functional Programming](#functional-programming) - [Game Development](#game-development) - [GUI](#gui) @@ -250,6 +251,17 @@ A curated list of awesome Java frameworks, libraries and software. * [documents4j](http://documents4j.com) - API for document format conversion using third-party converters such as MS Word. * [jOpenDocument](http://www.jopendocument.org/) - Processes the OpenDocument format. +## Formal Verification + +*Formal-methods tools: proof assistants, model checking, symbolic execution etc.* + +* [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. Can generate JML specs based on the invariants. +* [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) ([repository](http://babelfish.arc.nasa.gov/hg/jpf/jpf-core/)) - "The Swiss army knife of Java verification." A model checker for Java (bytecode) and more. By NASA +* [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Setects 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://jmlspecs.sourceforge.net/) ([alternate website](http://openjml.github.io/))- Formal methods tool for Java and the Java Modeling Language (JML). OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. + ## Functional Programming *Libraries that facilitate functional programming.* From 6d2bc395fa339290aaa188fd7e9ee499ac2d0257 Mon Sep 17 00:00:00 2001 From: pron Date: Wed, 28 Oct 2015 12:45:48 +0200 Subject: [PATCH 2/5] Add jCUTE --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 6b4f33b..e27402e 100644 --- a/README.md +++ b/README.md @@ -258,6 +258,7 @@ A curated list of awesome Java frameworks, libraries and software. * [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. Can generate JML specs based on the invariants. * [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) ([repository](http://babelfish.arc.nasa.gov/hg/jpf/jpf-core/)) - "The Swiss army knife of Java verification." A model checker for Java (bytecode) and more. By NASA +* [jCUTE](https://github.com/osl/jcute) - The Java Concolic Unit Testing Engine (jCUTE) automatically generates unit tests for Java programs. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving. See also [CATG](https://github.com/ksen007/janala2). * [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Setects 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://jmlspecs.sourceforge.net/) ([alternate website](http://openjml.github.io/))- Formal methods tool for Java and the Java Modeling Language (JML). OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. From 3138868562e1dc5e82831b9b04bce9c218a03d83 Mon Sep 17 00:00:00 2001 From: pron Date: Thu, 29 Oct 2015 12:54:19 +0200 Subject: [PATCH 3/5] Apply corrections suggested by @akullpp --- README.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index e27402e..70ba5c1 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,6 @@ A curated list of awesome Java frameworks, libraries and software. ## Code Analysis *Tools that provide metrics and quality measurements.* -* [Checker Framework](http://types.cs.washington.edu/checker-framework/) - Enhances Java’s type system to make it more powerful and useful. * [Checkstyle](https://github.com/checkstyle/checkstyle) - Static analysis of coding conventions and standards. * [Error Prone](https://github.com/google/error-prone) - Catches common programming mistakes as compile-time errors. * [FindBugs](http://findbugs.sourceforge.net/) - Static analysis of bytecode to find potential bugs. @@ -255,13 +254,15 @@ A curated list of awesome Java frameworks, libraries and software. *Formal-methods tools: proof assistants, model checking, symbolic execution etc.* -* [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. Can generate JML specs based on the invariants. +* [CATG](https://github.com/ksen007/janala2) - A concolic unit testing engine for Java programs. 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) ([repository](http://babelfish.arc.nasa.gov/hg/jpf/jpf-core/)) - "The Swiss army knife of Java verification." A model checker for Java (bytecode) and more. By NASA -* [jCUTE](https://github.com/osl/jcute) - The Java Concolic Unit Testing Engine (jCUTE) automatically generates unit tests for Java programs. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving. See also [CATG](https://github.com/ksen007/janala2). -* [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Setects nonconformances between Java code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected +* [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. +* [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://jmlspecs.sourceforge.net/) ([alternate website](http://openjml.github.io/))- Formal methods tool for Java and the Java Modeling Language (JML). OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. +* [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 From 1d3f52a408903264c1b8026fd46fa72c60865f9f Mon Sep 17 00:00:00 2001 From: pron Date: Sat, 31 Oct 2015 08:35:56 +0200 Subject: [PATCH 4/5] 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. From 0d853c8492aa8401a3a5fa06f89bffa3de7512e8 Mon Sep 17 00:00:00 2001 From: pron Date: Sat, 31 Oct 2015 08:38:40 +0200 Subject: [PATCH 5/5] Fixes --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 5e80358..c277beb 100644 --- a/README.md +++ b/README.md @@ -254,13 +254,13 @@ 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) - 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. +* [CATG](https://github.com/ksen007/janala2) - Concolic unit testing engine. Automatically generates unit tests using formal methods. +* [Checker Framework](http://types.cs.washington.edu/checker-framework/) - Pluggable type systems. 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. +* [Java Modeling Language (JML)](http://www.jmlspecs.org) - Behavioral interface specification language that can be used to specify the behavior of code 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 verification tools. +* [Java Path Finder (JPF)](http://babelfish.arc.nasa.gov/trac/jpf) - JVM formal verification tool containing a model checker and more. Created by NASA. * [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. +* [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. * [OpenJML](http://openjml.github.io/) - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.