Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Tools

PSYCO

PSYCO generates and verifies symbolic behavioral interfaces for software components using a combination of multiple dynamic and static analysis techniques: active automata learning, concolic execution, static code analysis, symbolic search, predicate abstraction, and model-based testing.

jConstraints

JConstraints is a constraint solver abstraction layer for Java. It provides an object representation for logic expressions, unified access to different SMT and interpolation solvers, and some useful tools and algorithms for working with constraints. While JConstraints has been developed for JDart, it is maintained as a stand-alone library that can be used independently. Currently, plugins exist for connecting to the SMT solver Z3, the interpolation solver SMTInterpol, the meta-heuristic based constraint solver Coral.

JDart

JDart is a concolic execution engine Java based on Java PathFinder (JPF). JDart can be used to generate test cases as well as the symbolic summaries of methods. The tool executes Java programs with concrete and symbolic values at the same time and records symbolic constraints describing all the decisions along a particular path of the execution. These path constraints are then used to find new paths in the program. Concrete data values for exercising these paths are generated using a constraint solver.

LearnLib

LearnLib is a library for automata learning and experimentation. Its modular structure allows users to configure their tailored learning scenarios, which exploit specific properties of the envisioned applications. As has been shown earlier, exploiting application-specific structural features enables optimizations that may lead to performance gains of several orders of magnitude, a necessary precondition to make automata learning applicable to realistic scenarios.

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.

CVC4-TurnKey and Z3-TurnKey

CVC4-TUrnKey and Z3-TurnKey are self-contained distributions of the open souce Z3 and CVC4 Theorem Provers and their Java APIs. Using this distribution, developers can seamlessly integrate CVC4 and Z3 into their JVM applications without forcing downstream users to install the respective support libraries. The distributions are available on Maven Central.



Nebeninhalt

logo

Kontakt:

Ute Joschko 
Sekretariat Lehrstuhl 14

Telefon:
(+49)231 755-7953

Fax:
(+49)231 755-7936

Anschrift

Technische Universität Dortmund

Fakultät für Informatik 
LS 14 - Software Engineering

Otto-Hahn-Str. 12
44227 Dortmund