/dash

Java implementation of a subset of DASH

Primary LanguageJava

#DASH for Java Creative Commons Attribution 4.0 International License This is a Java implementation of a subset of DASH developed by Kasper Føns and Jacob Hougaard during their master thesis, A study of the DASH algorithm for software property checking, created while studying Computer Science at Aarhus University.

##What is DASH? DASH is an algoritmh that can check if a program satisfies a given safety property. DASH both concretly and symbolically executes the program being tested. A unique feature of the DASH algorithm is that it uses only test generation operations, and it refines and maintains a sound program abstraction as a consequence of failed test generations. DASH was developed by Microsoft for analyzing device drivers written in the programming language C.

##Implementation The implementation supports interprocedural analysis of integer programs. There are numerous examples in the tests directory. It does not support pointers (as DASH does), objects, doubles and many other features.

###Requirements for running

Windows 64bit and a 64bit version of Java is required since Z3, a theorem prover, was built for Windows 64bit. If you build the Z3 binary yourself, the project should be able to run on Linux as well. The Z3 binaries in the repository is built from the unstable branch of Z3 with the commit hash b1b349f49662d16c87060f82ddcf8204ce4f7b. Loading of libz3 and dependencies are performed in Native.java. Building newer versions of Z3 might require that the Z3 JNI wrappers are upgraded as well.

###Run all tests Executing all the tests in the project can be achieved by invoking gradle: gradlew test. It is easy to add new tests to the project.

Graphs can be generated for each iteration of DASH by setting the log level to trace in log4j.xml. Be prepared to take a coffee break, as graph output is not fast. Notice that GraphViz dot is used to generate the graphs, and the binary contained in the repository is built for Windows.

##Thesis The thesis is written in LaTeX and can be built on Windows by the script thesis/build.bat. For convenience it is also found in compiled form: A study of the DASH algorithm for software property checking.

##License All work performed by third party is licensed under their respective licenses.

Work performed by us is licensed under a Creative Commons Attribution 4.0 International License.. For fun, we would appreciate if you notified us if you use this project.