@martinschaef martinschaef released this Jan 17, 2017 · 41 commits to devel since this release

Assets 3

Release for the Lpar submission.
To run the example from Section 2 perform the following steps:

wget https://gist.githubusercontent.com/martinschaef/0e8244f91670244e4569b366474bbf30/raw/4e62e8e7ad5b12d01e2289f0947f090b972bfae9/Maun.java
wget https://github.com/jayhorn/jayhorn/releases/download/v0.5.1/jayhorn.jar
mkdir tmp
javac Maun.java -d tmp
java -jar jayhorn.jar -j tmp -solution

The output will show that the program is safe and the invariants for each used Class type. The printing is not very polished, so some variables only have their skolemized name starting with an underscore.

Assets 3

JayHorn tries to find a proof that certain bad states in a Java program are never reachable. Bad states are states where an assert statement fails or an exceptions leaves the main method. JayHorn tracks runtime assertions NullPointerException, IndexOutOfBoundsException, and ClassCastException. Other RuntimeExceptions have to be modeled by the user using assertions.

Changes

  • Improved precision
  • Added command line arguments for inlining
  • Added Spacer backend
  • Bug fixes

Soundness still limited to programs that are:

  • single-threaded,
  • do not use dynamic class loading,
  • have no fancy static initializers.

And there may still be bugs.

How to run

wget https://github.com/jayhorn/jayhorn/releases/download/v0.4.1/jayhorn.jar
wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/jayhorn/src/test/resources/horn-encoding/classics/SatAckermann01.java
mkdir out
javac SatAckermann01.java -d out/
java -jar jayhorn.jar -j out/

@martinschaef martinschaef released this Oct 6, 2016 · 104 commits to master since this release

Assets 3

JayHorn tries to find a proof that certain bad states in a Java program are never reachable. Bad states are states where an assert statement fails or an exceptions leaves the main method. JayHorn tracks runtime assertions NullPointerException, IndexOutOfBoundsException, and ClassCastException. Other RuntimeExceptions have to be modeled by the user using assertions.

Changes

  • Bug fixes
  • Updated Eldarica

Soundness still limited to programs that are:

  • single-threaded,
  • do not use dynamic class loading,
  • have no fancy static initializers.

And there may still be bugs.

How to run

wget https://github.com/jayhorn/jayhorn/releases/download/v0.4.1/jayhorn.jar
wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/jayhorn/src/test/resources/horn-encoding/classics/SatAckermann01.java
mkdir out
javac SatAckermann01.java -d out/
java -jar jayhorn.jar -j out/

@martinschaef martinschaef released this Sep 24, 2016 · 126 commits to master since this release

Assets 3

JayHorn tries to find a proof that certain bad states in a Java program are never reachable. Bad states are states where an assert statement fails or an exceptions leaves the main method. JayHorn tracks runtime assertions NullPointerException, IndexOutOfBoundsException, and ClassCastException. Other RuntimeExceptions have to be modeled by the user using assertions.

Changes

  • Improved precision and added options to tune precision.
  • Fixed bugs that introduced unsoundness for static initializers
  • Verification now ensures that no uncaught exception leaves main.

Soundness still limited to programs that are:

  • single-threaded,
  • do not use dynamic class loading,
  • have no fancy static initializers.

And there may still be bugs.

How to run

wget https://github.com/jayhorn/jayhorn/releases/download/v0.4/jayhorn.jar
wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/jayhorn/src/test/resources/horn-encoding/classics/SatAckermann01.java
mkdir out
javac SatAckermann01.java -d out/
java -jar jayhorn.jar -j out/

@martinschaef martinschaef released this Sep 1, 2016 · 270 commits to master since this release

Assets 3

Changes

  • Improved soundness of previous release.
  • Fixed bug in handling of array fields
  • Fixed soundness issue when down-casting floats.

Soundness still limited to programs that are:

  • is single-threaded,
  • do not use dynamic class loading,
  • have no fancy static initializers.

And there may still be bugs.

How to run

wget https://github.com/jayhorn/jayhorn/releases/download/v0.3/jayhorn.jar
wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/jayhorn/src/test/resources/horn-encoding/classics/SatAckermann01.java
mkdir out
javac SatAckermann01.java -d out/
java -jar jayhorn.jar -j out/

@martinschaef martinschaef released this Aug 12, 2016 · 300 commits to master since this release

Assets 3

Modulo bugs, this version should be sound for Java that:
• is single-threaded,
• doesn't do dynamic class loading,
• has no fancy static initializers.

Pre-release

@martinschaef martinschaef released this Jul 13, 2016

Assets 3

Pre-release

This is a pre-release and known to be unsound due to several bugs.

Requirements

Java 8

Usage:

Either download the jayhorn.jar and cd into the directory of the jar, or build the jar from source as follows:

unzip jayhorn-0.1alpha.zip
cd jayhorn-0.1alpha/jayhorn/
gradle jar
cd build/libs

Now download and compile an example such as:

wget https://raw.githubusercontent.com/jayhorn/jayhorn/devel/jayhorn/src/test/resources/horn-encoding/simple1/Sat01.java
mkdir out
javac Sat01.java -d out

And run JayHorn on the compiled example:

java -jar jayhorn.jar -j out

Your output should end with

SAFETY VERIFICATION RESULT ... SAFE