Software for the 21st century
The AQUA group works on formal methods in software engineering. The one overarching question that drives our works is:
How can we ensure that a software system meets our requirements in the intended operation environment?
We work in four working directions:
- modeling assumptions on the intended operation environment,
- formalizing expectations into testable requirements,
- checking requirements on a system under the made assumptions, and
- supporting the corresponding tasks with tools, processes, and standards.
Safe Autonomous Systems
Please confirm video activation.
After activation, cookies will be set and data is sent to YouTube (Google).
To the Google Privacy Policy
We frequently base our teaching on our research (e.g., for model learning, symbolic execution, or for deveoping and testing automotive software). This allows students to get hands-on experience with the application of formal methods in the context of software engineering. We develop multiple software systems and frameworks that serve as case studies in our labs and courses:
- Autonomous Vehicle Lab (AV model vehicles for learning about developing and testing software for autonomous robotic systems)
- BoardGameWork (a framework for learning application development by developing board games in Kotlin)
- BoardGame Server (a SpringBoot web application for playing Pachisi and similar games in the browser for learning a.o. enterprise application patterns)
- BoardGame Editor (a Cinco meta-model from which an editor for Pachisi boards and rulesets can be generated)
- Very Insecure Web Application (a PHP web application for learning about injection attacks and pen testing)
World Class Research Tools for Model Learning and Software Verification
Robust research tools are a cornerstone for scaling formal methods towards industrial applications. The group develops multiple research tools, mainly for dynamic symbolic execution and model learning. To compete, compare, and collaborate with other researchers, we compete with our tools in SV-COMP and co-organize the RERS challenge.
We believe in open science and make our tools available as open source software. We strive to provide reproduction packages and benchmark suites for our results and engange in the national research data infrastructure (NFDI) to develop corresponding standards.
News
Dominik Schmid and Malte Mues visit Dagstuhl seminar on research methods
Dominik Schmid and Malte Mues visit Dagstuhl seminar on research methods
Robin Philipp defends Doctoral Dissertation
Robin successfully defended his dissertation project on methods for validating the perception of automated driving systems
EATCS Best ETAPS Paper Award for Joint Publication
Our TACAS 2024 paper “Scalable Tree-Based Register Automata Learning” was awarded the Best ETAPS Paper Award.
GDart wins BRONZE in SV-COMP 2024 for Java
Our dynamic symbolic execution GDart wins BRONZE in this year's Software Verification competition for the Java category.
Marcel Altendeitering defends Doctoral Dissertation
Marcel successfully defended his dissertation titled "Design Principles for Data Quality Tools".
DFG funding for project StdLearnLib
The StdLearnLib project ensures the continued development and expansion of the de-facto standard library in automata learning, LearnLib.
Autonomous Racing Showcased on AADC Model Car
At the university's 2023 open house event, AQUA group presented its work on autnomous driving on 1:8 scale model cars. Using the Jarvic racing…
NFDI4Ing seed funding for project ReReSo
Project ReReSo, funded by NFDI4Ing, aims at improving the reusability of research software through standardized data formats and tool interfaces.
GDart wins SILVER in SV-COMP 2023 for Java
Our dynamic symbolic execution GDart wins SILVER in this year's Software Verification competition for the Java category.
Malte Mues defends Doctoral Dissertation
Malte successfully defended his dissertation project on the integration of dynamic symbolic execution and multi-color taint analysis.
BMBF funding for Project QuARum
The QuARUm project, a collaboration between Constructor University and TU Dortmund University, aims to develop a low-code platform for geoscientists.
AQUA featured in CS@ TU Dortmund promotional video
Our research and teaching on software engineering for autonomous driving is featured in the promotional video of the CS department of TU Dortmund!
DFG funding for project STING
The STING project researches formal methods for finding exploits in Web applications.
Fabian Bruckner defends Doctoral Dissertation
Fabian successfully defended his dissertation project in which he developed concepts for enforcing data usage control requirements in DSLs.
JDart wins GOLD in SV-COMP 2022 for Java
Our dynamic symbolic execution JDart wins GOLD in this year's Software Verification competition for the Java category.
BMBF funding for project KomDatis
The projects will develop a general data escrow concept in a collaboration with Fraunhofer ISST and DKSR.
ACM Distinguished Paper Award for ASE 2021
Paper "Data-driven design and evaluation of SMT meta-solving strategies: balancing performance, accuracy, and cost" receives Distinguished Paper Award
Falk Howar receives Amazon Research Award
The funded project aims at scaling symbolic execution for the Java VirtualMachine.
JDart wins SILVER in SV-COMP 2021 for Java
Our dynamic symbolic execution JDart wins SILVER in this year's Software Verification competition for the Java category.
PG 625 "Development of Automated Tools for Solving CTFs" receives P5 Award
PG 625 "Development of Automated Tools for Solving CTFs", organized by the AQUA group at TU Dortmund University, wins this year's P5 Competition
