awesome/java
1
0
Fork 0
mirror of https://github.com/akullpp/awesome-java.git synced 2025-02-17 15:55:19 -05:00
Code Activity

Merge pull request #236 from pron/master

Browse source 
Add formal verification category
This commit is contained in:
Andreas Kull 2015-11-01 11:13:25 +01:00
commit 316e27abe3
1 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
README.md
View file

@ -23,6 +23,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)
@ -110,7 +111,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.
@ -267,6 +267,20 @@ 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.*
* [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) - 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 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.
## Functional Programming
*Libraries that facilitate functional programming.*