Dynamic Symbolic Execution for the JVM.
The repository contains the GDart-LLVM symbolic tracer (which is implemented as a Truffle instrument), support files, and the packaging scripts the combine it with the DSE engine and dependencies to obtain a standalone, SV-COMP-compliant tool.
JDart is a tool for performing concolic execution on a Java program. It is written as an extension to NASA Java Pathfinder (JPF). The aim of concolic execution is to explore additional behavior in the program by generating input values which will result in a different path being taken through a program (or method).
Symbolic Path Recording During Testing.
DSE (dynamic symbolic execution) is a generic dynamic symbolic execution. Some components of DSE were originally developed as part of JDart, first at NASA Ames Research Center, and later at TU Dortmund University.
LearnLibs purpose is to provide a framework for research on automata learning algorithms as well as for their application in practice.
RALib is a library for active learning algorithms for register automata (a form of extended finite state machines). RALib is developed as an extension to LearnLib. It implements the SL* algorithm presented in Sofia Cassel, Falk Howar, Bengt Jonsson, Bernhard Steffen: Learning Extended Finite State Machines. SEFM 2014: 250-264.
jConstraints is a library for modeling expressions and for interacting with constraint solvers.
Z3-TurnKey repackages the Z3 SMT solver and its Java API into a Java library that does not require Z3 to be manually installed on a host system. Using this library, Z3 can be used by JVM application like a pure Java dependency.
The CVC4 Theorem Prover is a widely used SMT solver that is written in C and C++, wrapping a large number of open source sub-solvers and libraries. The authors provide a Java API, however, it is not trivial to set up in a Java project. This project aims to solve this issue.
BoardGameWork is a framework for creating 2D board game applications. It is currently used in our teching (Software Lab) as a framework for students.