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