Selected (P)reprints

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
ICAART 2024, to appear
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
submitted
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

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¹ 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 ²
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³
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

Footnotes

(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.