doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Stať ve sborníku

10.1007/978-3-031-27481-7_5

Katedra číslicového návrhu

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.

Stať ve sborníku

10.1007/978-3-030-94583-1_12

Katedra číslicového návrhu

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.

Stať ve sborníku

10.1007/978-3-030-50995-8_5

Katedra číslicového návrhu

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.