Skip to content
Automatically discover time related errors
Branch: development
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
code-instrumentation
correct-time-behavior
daikon-instrumentation
debugger
evaluation
intermediate-model
java-parser
parallel-control-flow-graph
server
time-annotation
uppaal-library
usage
xal
.gitignore
README.md
constraint_kafka_4290_fix.conf
pom.xml

README.md

Purpose

The following project contains the code of the approach proposed for FormaliSE 2018

How to install

In order to package the project call

mvn clean package

If you do not like tests:

mvn clean package -DskipTests

How to use

Dependency

First, you need to install Z3 following this link. It is important to compile Z3 with the flag --java. Once Z3 is compiled, copy the following files in the same folder of the jar file created in the How to install section:

  • com.microsoft.z3.jar
  • z3 executable
  • dynamic libraries (e.g. libz3java.dylib on OSX)

Running it on file

First you need to index the project with

java -cp usage-0.5.jar smt.Indexing [project_name] [root_path]

This will execute the approach explained in the SCAM 2017 paper and it will extract user defined time related methods.

If you are not interested in compute user-defined time method, you can directly execute the verification of a file with the following command:

java -cp usage-0.5.jar smt.SingleFile [file_path] [project_root] [project_name]

Run the Experiment

Inside the evaluation folder there are data (except the open source projects) and files used in our experiments. Currently, the scripts to automatically clone the projects and run the evaluation support only macOS. The experiment can be run executing the run.sh script.

File summary contains a summary of our experiment in a excel table format. Folder results contains the output of our tool per project.

You can’t perform that action at this time.