Railway Scheduling Using Boolean Satisfiability Modulo Simulations
Authors
Kolárik, T.; Ratschan, S.
Year
2023
Published
Formal Methods. Springer, Cham, 2023. p. 56-73. ISSN 0302-9743. ISBN 978-3-031-27480-0.
Type
Proceedings paper
Departments
Annotation
Railway scheduling is a problem that exhibits both non-
trivial discrete and continuous behavior. In this paper, we model this
problem using a combination of SAT and ordinary differential equations
(SAT modulo ODE). In addition, we adapt our existing method for solv-
ing such problems in such a way that the resulting solver is competitive
with methods based on dedicated railway simulators while being more
general and extensible.
Fast Three-Valued Abstract Bit-Vector Arithmetic
Authors
Onderka, J.; Ratschan, S.
Year
2022
Published
23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. Basel: Springer Nature Switzerland AG, 2022. p. 242-262. ISSN 0302-9743. ISBN 978-3-030-94582-4.
Type
Proceedings paper
Departments
Annotation
Abstraction is one of the most important approaches for reducing the number of states in formal verification. An important abstraction technique is the usage of three-valued logic, extensible to bit-vectors. The best abstract bit-vector results for movement and logical operations can be computed quickly. However, for widely-used arithmetic operations, efficient algorithms for computation of the best possible output have not been known up to now.
In this paper, we present new efficient polynomial-time algorithms for abstract addition and multiplication with three-valued bit-vector inputs. These algorithms produce the best possible three-valued bitvector output and remain fast even with 32-bit inputs.
To obtain the algorithms, we devise a novel modular extreme-finding technique via reformulation of the problem using pseudo-Boolean modular inequalities. Using the introduced technique, we construct an algorithm for abstract addition that computes its result in linear time, as well as a worst-case quadratic-time algorithm for abstract multiplication. Finally, we experimentally evaluate the performance of the algorithms, confirming their practical efficiency.
SAT Modulo Differential Equation Simulations
Authors
Kolárik, T.; Ratschan, S.
Year
2020
Published
Tests and Proofs. Cham: Springer, 2020. p. 80-99. ISSN 0302-9743. ISBN 978-3-030-50994-1.
Type
Proceedings paper
Departments
Annotation
Differential equations are of immense importance for modeling physical phenomena, often in combination with discrete modeling formalisms. In current industrial practice, properties of the resulting models are checked by testing, using simulation tools. Research on SAT solvers that are able to handle differential equations has aimed at replacing tests by correctness proofs. However, there are fundamental limitations to such approaches in the form of undecidability, and moreover, the resulting solvers do not scale to problems of the size commonly handled by simulation tools. Also, in many applications, classical mathematical semantics of differential equations often does not correspond well to the actual intended semantics, and hence a correctness proof wrt. mathematical semantics does not ensure correctness of the intended system.
In this paper, we head at overcoming those limitations by an alternative approach to handling differential equations within SAT solvers. This approach is usually based on the semantics used by tests in simulation tools, but still may result in mathematically precise correctness proofs wrt. that semantics. Experiments with a prototype implementation confirm the promise of such an approach.