Tools

Program Analysis

GDart

Dynamic Symbolic Execution for the JVM.

License: Apache License 2.0
GitHub: tudo-aqua/gdart

GDart-LLVM

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.

License: GNU General Public License v2.0
GitHub: tudo-aqua/gdart-llvm 

JDart

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).

License: Apachae License 2.0
GitHub: tudo-aqua/jdart 

SPouT

Symbolic Path Recording During Testing.

License: GNU General Public License (GPL)
GitHub: tudo-aqua/spout 

DSE

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.

License: Apache License 2.0
GitHub: tudo-aqua/ds

Model Learning

LearnLib

LearnLibs purpose is to provide a framework for research on automata learning algorithms as well as for their application in practice.

License: Apache License 2.0
GitHub: tudo-aqua/learnlib

RaLib

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.

License: Apache License 2.0
GitHub: LearnLib/ralib

Constraint Solving

JConstraints

jConstraints is a library for modeling expressions and for interacting with constraint solvers.

License: Apache License 2.0
GitHub: tudo-aqua/jconstraints

Z3 TurnKey

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.

License: ISC License
GitHub: tudo-aqua/z3-turnkey
Library: pkg:maven/tools.aqua/z3-turnkey

CVC4 TurnKey

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.

License: ISC License
GitHub: tudo-aqua/cvc4-turnkey
Library: pkg:maven/io.github.tudo-aqua/cvc4-turnkey-gpl, pkg:maven/io.github.tudo-aqua/cvc4-turnkey-permissive

Safety of Autonomous Systems

STARS

STARS (Scenario-Based Testing of Autonomous Robotic Systems) is a formal framework for coverage analysis of test data of autonomous robotic systems.

GitHub: tudo-aqua/stars
Artifact: 10.5281/zenodo.8131947

Teaching

BoardGameWork

BoardGameWork is a framework for creating 2D board game applications. It is currently used in our teching (Software Lab) as a framework for students.

License: Apache License 2.0
GitHub: tudo-aqua/bgw
Library:  pkg:maven/tools.aqua/bgw-gui, pkg:maven/tools.aqua/bgw-net-common,  pkg:maven/tools.aqua/bgw-net-client, pkg:maven/tools.aqua/bgw-net-server