Running research projects
- UnRAVeL: UNcertainty and Randomness in Algorithms, VErification and Logic (Research Training Group, German Research Foundation)
- RealySt: Reachability Analysis for Stochastic Hybrid Systems (German Research Foundation)
- SMT-ART: SMT Arithmetic Reasoning Techniques (German Research Foundation)
- EUGAIN: European Network for Gender Balance in Informatics (EU COST Action CA19122)
- EuroProofNet: European Research Network on Formal Proofs (EU COST Action CA20111)
- REMARO: Reliable AI for Marine Robotics (EU HORIZON2020 ITN)
- Sim4Dialog (IN4climate.NRW)
- SMT-RAT: SAT-Modulo-Theories Real Arithmetic Toolbox
- CArL: Computer ARithmetic Library
- Embedding Machine Learning within Quantifier Elimination Procedures
Completed research projects
- ARC: Automated Reasoning in the Class (EU Erasmus+, KA203 – Strategic Partnerships for Higher Education)
- Towards an Integrated Data Science of Complex Natural Systems
- Digitalization and Energy Optimization in Buildings using Artificial Intelligence (BMWi/DEOKI industrial project with MeteoViva)
- Safety Verification for Mixed Discrete-Continuous Automotive systems (industrial project with Ford)
- CAP Sino-German Project
- SC-Square: Satisfiability Checking and Symbolic Computation (H2020-FETOPEN CSA)
- Optimizing the Performance of Robot Fleets in Production Logistics Scenarios using SMT (RWTH Seed Funds)
- Simulink Formal Verification (industrial project with Ford)
- HyPro I: A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations (German Research Council)
- HyPro II: A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations (German Research Council)
- SMT4ABS: Combining SMT Solving with Type Checking for Real-Time ABS Programs (DAAD ppp)
- OASys: Online Algorithms for Optimal Control of Hybrid Propulsion Systems (German Research Council)
- CEBug: Counter Example Generation for Stochastic Systems using Bounded Model Checking (German Research Council)
- HySmart: Hybrid Systems Modeling and Analysis with Rewriting Techniques (DAAD ppp)
- AlgoSyn: Algorithmic synthesis of reactive and discrete-continuous systems (Research Training Group)
- ROCKS: RigorOus dependability analysis using model ChecKing techniques for Stochastic systems (Dutch-German Bilateral Cooperation Program)