| 2026 | VMCAI | Input-Based Three-Valued Abstraction Refinement. | Jan Onderka, Stefan Ratschan |
| 2025 | CADE | SMT and Functional Equation Solving over the Reals: Challenges from the IMO. | Chad E. Brown, Karel Chvalovsk, Mikols Janota, Mirek Olsk, Stefan Ratschan |
| 2024 | ICAART | Multi-Agent Path Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic. | Toms Kolrik, Stefan Ratschan, Pavel Surynek |
| 2023 | FM | Railway Scheduling Using Boolean Satisfiability Modulo Simulations. | Toms Kolrik, Stefan Ratschan |
| 2023 | IROS | LQR-Trees with Sampling Based Exploration of the State Space. | Jir Fejlek, Stefan Ratschan |
| 2023 | MFCS | Deciding Predicate Logical Theories Of Real-Valued Functions. | Stefan Ratschan |
| 2022 | ICRA | Computing Funnels Using Numerical Optimization Based Falsifiers. | Jir Fejlek, Stefan Ratschan |
| 2022 | VMCAI | Fast Three-Valued Abstract Bit-Vector Arithmetic. | Jan Onderka, Stefan Ratschan |
| 2020 | TAP | SAT Modulo Differential Equation Simulations. | Toms Kolrik, Stefan Ratschan |
| 2011 | MFCS | Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable. | Peter Franek, Stefan Ratschan, Piotr Zgliczynski |
| 2010 | CAV | Safety Verification for Probabilistic Hybrid Systems. | Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn |
| 2010 | TAMC | Safety Verification of Non-linear Hybrid Systems Is Quasi-Semidecidable. | Stefan Ratschan |
| 2009 | TAP | Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate. | Stefan Ratschan, Jan-Georg Smaus |
| 2008 | ICINCO | Recursive and Backward Reasoning in the Verification on Hybrid Systems. | Stefan Ratschan, Zhikun She |
| 2007 | VMCAI | Language-Based Abstraction Refinement for Hybrid System Verification. | Felix Klaedtke, Stefan Ratschan, Zhikun She |
| 2006 | AISC | Constraints for Continuous Reachability in the Verification of Hybrid Systems. | Stefan Ratschan, Zhikun She |
| 2005 | ATVA | Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. | Werner Damm, Guilherme Pinto, Stefan Ratschan |
| 2003 | CP | Solving Existentially Quantified Constraints with One Equality and Arbitrarily Many Inequalities. | Stefan Ratschan |
| 2002 | AISC | Continuous First-Order Constraint Satisfaction. | Stefan Ratschan |
| 2002 | CP | Continuous First-Order Constraint Satisfactionwith Equality and Disequality Constraints. | Stefan Ratschan |