From c9383b28ace64a631a47bc40b815ed4ee0e6df32 Mon Sep 17 00:00:00 2001 From: heldev Date: Wed, 2 Oct 2019 20:09:36 -0400 Subject: [PATCH] Java Path finder new official URL The old link doesn't work (it requires authorization) so people from the official google group (again linked from the old sourceforge homepage http://javapathfinder.sourceforge.net ) pointed to the new URL https://groups.google.com/forum/#!topic/java-pathfinder/F2Fq3TjEYIs --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 1ab65a5..ea3441b 100644 --- a/README.md +++ b/README.md @@ -368,7 +368,7 @@ A curated list of awesome Java frameworks, libraries and software. - [CATG](https://github.com/ksen007/janala2) - Concolic unit testing engine. Automatically generates unit tests using formal methods. - [Checker Framework](https://types.cs.washington.edu/checker-framework) - Pluggable type systems. Includes nullness types, physical units, immutability types and more. - [Daikon](https://plse.cs.washington.edu/daikon) - Detects likely program invariants and generates JML specs based on those invariants. -- [Java Path Finder (JPF)](https://babelfish.arc.nasa.gov/trac/jpf) - JVM formal verification tool containing a model checker and more. Created by NASA. +- [Java Path Finder (JPF)](https://github.com/javapathfinder/jpf-core) - JVM formal verification tool containing a model checker and more. Created by NASA. - [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Detects inconsistencies between code and JML specification through feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected. - [KeY](https://key-project.org) - 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](https://openjml.github.io) - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.