Contact me () if you have any comment or question regarding the papers below. For a more complete list of accepted refereed publications see my CV.

Tomáš Kolárik, Stefan Ratschan, and Pavel Surynek

**Multi-Agent Path Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic**

Proc, of the 16th International Conference on Agents and Artificial Intelligence (ICAART), Volume 1, pp. 47--58

ArXiV

Stefan Ratschan

**Deciding Predicate Logical Theories of Real-Valued Functions**

Proc. of the 48th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2023

DOI ArXiV

Jiří Fejlek and Stefan Ratschan

**LQR-trees with Sampling Based Exploration of the State Space**

Proc. of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2023

ArXiV DOI

Enrico Lipparini and Stefan Ratschan

**Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem**

Proceedings of the NASA Formal Methods Symposium, Springer LNCS 13903, 2023

ArXiV DOI BIB

Tomáš Kolárik and Stefan Ratschan

**Railway Scheduling Using Boolean Satisfiability Modulo Simulations**

Proc. FM 2023, Springer LNCS 14000

ArXiV (extended version) DOI BIB

Jiří Fejlek and Stefan Ratschan

**Computation of Feedback Control Laws Based on Switched Tracking of Demonstrations**

European Journal of Control, Volume 80, 2024

DOI ArXiV code and experiments

Jan Onderka and Stefan Ratschan

**Fast Three-Valued Abstract Bit-Vector Arithmetic**

Proc. VMCAI 2022, Springer LNCS 13182

DOI artifact (by Jan Onderka)

Jiří Fejlek and Stefan Ratschan

**Computing Funnels Using Numerical Optimization Based Falsifiers**

ICRA 2022 - IEEE International Conference on Robotics and Automation, pp. 4318-4324, IEEE, 2022

ArXiV DOI BIB

Tomáš Kolárik and Stefan Ratschan

**SAT Modulo Differential Equation Simulations**

14th International Conference on Tests and Proofs, Springer LNCS 12165, 2020

DOI PDF BIB

Jan Kuřátko and Stefan Ratschan

**Solving Reachability Problems by a Scalable Constrained Optimization Method**

Optimization and Engineering, Volume 21, 2020, pp. 215-239

DOI BIB

Stefan Ratschan

** Converse Theorems for Safety and Barrier Certificates **

IEEE Trans. on Automatic Control, Volume 63, Issue 8, 2018

DOI ArXiv

Stefan Ratschan

** Simulation Based Computation of Certificates for Safety of Dynamical Systems **

Proc. FORMATS 2017, Springer LNCS 10419

DOI ArXiv BIB

Milan Hladík, and Stefan Ratschan

**Efficient Solution of a Class of Quantified Constraints with Quantifier
Prefix Exists-Forall**

Mathematics in Computer Science, Volume 8, Issue 3, 2014, pp. 329-340

DOI ArXiv BIB

Jan Kuřátko, and Stefan Ratschan

**Combined Global and Local Search for the Falsification of Hybrid Systems**

Proc. FORMATS 2014, Springer LNCS 8711

DOI extended version BIB

Peter Franek, and Stefan Ratschan

**Effective Topological Degree Computation Based on Interval Arithmetic**

Mathematics of Computation, Volume 84, 2015, pp. 1265-1290

DOI arXiv

Peter Franek, Stefan Ratschan, and Piotr Zgliczynski

**Quasi-decidability of a Fragment of the First-order Theory of Real Numbers**

Journal of Automated Reasoning, Volume 72, 2016, pp. 157-185.

DOI ArXiv BIB

Stefan Ratschan

**Safety Verification of Non-linear Hybrid Systems is Quasi-decidable**

Formal Methods in System Design, Volume 44, 2014, Issue 1, pp 71-90

DOI PDF
BIB

Tomáš Dzetkulič, and Stefan Ratschan**Incremental Computation of
Succinct Abstractions For Hybrid Systems**

FORMATS 2011, Springer LNCS 6919

DOI PDF BIB

Stefan Ratschan, and Zhikun She**Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-like
Functions**

SIAM J. Control and Optimization, Volume 48, Number 7, 2010,
pp. 4377-4394

DOI PDF

Tomáš Dzetkulič, and Stefan Ratschan**How to Capture Hybrid Systems
Evolution Into Slices of Parallel Hyperplanes**

ADHS'09: 3rd IFAC
Conference on Analysis and Design of Hybrid Systems

DOI
PDF
BIB

Stefan Ratschan, and Jan-Georg Smaus**Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate**

Proc. TAP: Tests and Proofs, Springer LNCS 5668, pp. 153-168, 2009

DOI PDF of
extended version BIB

Journal on Satisfiability, Boolean Modeling and Computation

Special Issue on SAT/CP Integration

Volume 1, 2007, 209-236

online PDF BIB

Henning Burchardt, and Stefan Ratschan**Estimating the Region of Attraction of Ordinary Differential Equations by Quantified Constraint Solving**

Proceedings of the 3rd WSEAS International Conference on DYNAMICAL SYSTEMS and CONTROL (CONTROL'07),

WSEAS Press, 2007, 241-246

PDF BIB

Stefan Ratschan, and Zhikun She**Constraints for Continuous Reachability in the Verification of Hybrid Systems**

Proc. 8th International Conference on artificial intelligence and symbolic computation, Springer
LNCS 4120, 196-210, 2006

DOI Postscript BIB

Werner Damm, Guilherme Pinto, and Stefan Ratschan**Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems**

International Journal of Foundations of Computer Science (IJFCS), Volume 18, Number 1, 2007

DOI Postscript PDF BIB

This is a revised and extended version of an article with the same authors and name that
appeared in the proceedings of ATVA'05, Springer LNCS 3707, 2005, DOI

Stefan Ratschan and Zhikun She**Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction
Refinement**

ACM Transactions in Embedded Computing Systems, Volume 6, Number
1, 2007

DOI Postscript BIB

This is a revised and extended version of an article with the same authors and name that
appeared in the proceedings of HSCC'05, Springer LNCS 3414, 2005 Springer

Stefan Ratschan**Solving Existentially Quantified Constraints with One Equality and Arbitrarily Many
Inequalities**

Proc. 9th International Conference on Principles and Practice of Constraint Programming,
Springer LNCS 2833, 2003

Postscript BIB Springer

Stefan Ratschan and Josep Vehí**Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods**

Robust Control Design 2003 -- Proceedings of the 4th IFAC Symposium

Patrizio Colaneri (ed.), Elsevier Science, 2004

Postscript BIB

Stefan Ratschan

**Efficient Solving of Quantified Inequality Constraints over the Real Numbers**

ACM Transactions on Computational Logic, Volume 7, Number 4, pp. 723-748, 2006

Original Paper Errata arXiv^{1} BIB

This is a revised and extended version of: Stefan Ratschan,
**Continuous First-Order Constraint Satisfaction**,
Artificial Intelligence, Automated Reasoning, and Symbolic Computation 2002,
Springer LNCS 2385, 2002

Stefan Ratschan**Continuous First-Order Constraint Satisfaction with Equality and Disequality Constraints**
^{2}

Proc. 8th International Conference on Principles and Practice of Constaint Programming,
Springer LNCS 2470, 2002

Postscript BIB Springer

Stefan Ratschan**Real First-Order Constraints are Stable with Probability One**

Draft.

Postscript

Stefan Ratschan**Search Heuristics for Box Decomposition Methods**

Journal Of Global Optimization, volume 24, number 1, 51-60, 2002

Postscript DOI BIB

Stefan Ratschan**Quantified Constraints Under Perturbation**

Journal of Symbolic Computation, volume 33, number 4, 493-505, 2002^{3}

Postscript DOI BIB

Stefan Ratschan**Convergent Approximate Solving of First-Order Constraints by Approximate Quantifiers**

ACM Transactions on Computational Logic.
volume 5, number 2, pages 264-281, 2004,

Postscript DOI BIB

Stefan Ratschan**Approximate Quantified Constraint Solving by Cylindrical Box Decomposition**

Reliable Computing, volume 8, number 1, 2002, 21-42.

Postscript DOI BIB

Stefan Ratschan**Uncertainty Propagation in Heterogenous Algebras for Approximate Quantified Constraint Solving**

Journal of Universal Computer Science, volume 6, number 9, 2000

Paper
Extended Abstract BIB

Stefan Ratschan and Luc Jaulin**Solving Composed First-Order Constraints From Discrete-Time Robust Control**

Proceedings of the Sixth Annual Workshop of the ERCIM Working Group on Constraints

2001

Postscript BIB

Stefan Ratschan**Applications of Quantified Constraint Solving**

Bibliography and Benchmark Problems

arXiv

- (1)
- @ ACM, (2006). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOCL, volume 7, number 4, Oct. 2006
- (2)
- The main theorem of this paper depends on Theorem 5.3.7 in A. Neumaier: Interval Methods for Systems of Equations, whose proof contains a gap, found by Alexandre Goldsztejn. The problem has been fixed in a diploma thesis by Peter Schodl at the University of Vienna.
- (3)
- This material has been published in Journal of Symbolic Computation, volume 33, number 4, 493-505, the only definitive repository of the content that has been certified and accepted after peer review. Copyright and all rights therein are retained by Academic Press. This material may not be copied or reposted without explicit permission.