Optimizing minimal counterexamples

Understanding Programming Bugs in Java Programs Using Counterexamples - Optimizing minimal counterexamples

Dependencies

Java PathFinder(JPF)

Java Bounded Model Checker(JBMC)

IDEA Intellij Community Edition

How to install

JPF and JBMC are required to install on your machine prior to clone this repository, please go to their github page for more details.

How to build

Once the repository is cloned, use Intellij or terminal to build under gradle environment:

./gradlew build

and run all tests by

./gradlew test

How to run

Run the following command:

java -jar [your RunJPF.jar path] [your example.jpf built]

An example of running can be shown as

java -jar build/RunJPF.jar src/examples/Racer.jpf

For JBMC, simply add jbmc.exe into your PATH variable(under Windows machine) and use the command in a terminal

jbmc [your java '.class' file path]

An example of running can be shown as (do not include .class suffix in argument)

jbmc src/main/java/Testing/Main

Example

An example of JPF output:

Demostration

The detailed demonstration of this seminar can be seen inside the PDF or PPT attached.