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

Theses

Dissertation theses

Constraint Solving

Level
Topic of dissertation thesis
Topic description

We develop software, theory, and algorithms that can solve mathematical constraints consisting of non-linear equalities and inequalities, conjunctions, disjunctions, and logical quantifiers. We apply the constraint solving technology in several areas (e.g., verification of complex systems, computation of Lyapunov functions), and offer a large range of thesis topics in the area.

More information:

Executable Specifications

Level
Topic of dissertation thesis
Topic description

One of the big drawbacks of classical methods for specifying software requirements is that it is difficult to check the consistency and adequacy of a given specification. The software engineering community has come up with various remedies to this situation (e.g., model based software engineering, agile software development, executable algebraic specification) that usually aim at allowing the user to see the actual behavior of a given specification as early as possible in the development process, but that makes compromises in terms of expressivity or precision. In the thesis, the student will design an executable formal specification language that fulfills two seemingly contradicting objectives:

• High modeling capabilities in terms of expressivity and precision

• Efficient execution

The key to achieving both objectives at the same time will be the design of annotations for the specification language that provide information necessary of efficient execution. Increasing user efforts in writing annotations will result in increasing efficiency of execution of the given specification.

Verification of Complex Systems

Level
Topic of dissertation thesis
Topic description

The Pendolino train from Prague to Ostrava had severe problems in its initial phase: from time to time it stopped in the middle of nowhere due to a software bug. Similar bugs have been the cause of more severe incidents, for example the crash of the Ariane 5 rocket in 1996. We are doing research that will help to avoid such problems in the future, and offer a large range of thesis topics in the area.

More information:

Bachelor theses

The influence of the type of arithmetic on the Korovin/Tsiskaridz/Voronkov algorithm for solving linear inequalities

Author
Tomáš Makara
Year
2013
Type
Bachelor thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
prof. Ing. Róbert Lórencz, CSc.
Summary
In this thesis we discuss solving of system of linear inequalities with Korovin/Tsiskaridz/Voronkov algorithm. We examine possibilities of using this algorithm with floating point arithmetic. Thesis contains description of original algorithm and descriptions of its modifications, which permit using floating point arithmetic. Thesis also contains implementation of algorithm and measuring of implementation performance.

Heuristics for interval constraint propagation

Author
Jakub Kottnauer
Year
2016
Type
Bachelor thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
doc. Ing. Ivan Šimeček, Ph.D.
Summary
A constraint is a relation between variables which reduces the set of values that can be assigned to a variable. A constraint safisfaction problem (CSP) is the problem of finding values for the variables in a given constraint that satisfy the constraint. The main goal of this thesis is to test the influence of various heuristics on the efficiency of solving numerical CSP problems by interval propagation. A solver written in the F# language utilizing the HC3 algorithm and a branch-and-prune algorithm was created, important aspects of the HC3 algorithm influencing its efficiency were found and then experiments with thirteen different heuristics were performed. The results found in the thesis can be used when deciding which heuristic to use for solving constraint satisfaction problems.

Automatic Function Synthesis Using SAT Modulo Theory Solvers

Author
Petr Nagy
Year
2023
Type
Bachelor thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Ing. Josef Vogel, CSc.
Summary
The bachelor's thesis is devoted to the cvc5 solver, an automatic theorem prover. Its primary goal is research into the possibilities of the cvc5 solver for automatic synthesis of functions and the use of this solver in practice. It examines its behavior using existing benchmark problems of cvc5 and of the SyGuS language, including its own examples, and concludes that cvc5 has very good potential for practical use. However, it also finds limitations, such as cvc5 does not support recursion yet. Currently, cvc5 is used for static code checking, but also for generating test cases. Another goal of this thesis was to create a graphical interface that will facilitate the use of cvc5 for function synthesis. The graphical interface was created after analyzing current solutions in such a way that it supports all functions of the solver as well as the creation and editing of the code itself.

Solving constraints with quantifier prefix exists-forall

Author
Pavel Frumert
Year
2016
Type
Bachelor thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Mgr. Jan Starý, Ph.D.
Summary
Goal of this thesis is experimental verification of method for constraints sol- ving. Efficiency of this method is proved on special QCSP instances where existencial quantifiers precede the universal ones. In addition we are handling with continuous domain of variables. Apart from basic satisfiability task we are also interested in specific solution of existencial-quantified variables. This method is implemented in wolfram mathematica software.

Master theses

Deadline Verification Using Model Checking

Author
Jan Onderka
Year
2020
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
doc. Ing. Jan Schmidt, Ph.D.
Summary
In this thesis, a new utility is presented for performing formal deadline checking of simple microcontroller programs at machine code level. The existing formal verification approaches and tools are studied and their weaknesses identified. Namely, source level techniques cannot guarantee cycle-count precise execution times, while machine code verification tools are few, not generally available, and usually heavily tailored to a specific processor, significantly reducing their usefulness. To counteract the weaknesses of current microcontroller verification tools, a novel hybrid approach is proposed and implemented. Machine code level model checking techniques are used for state space representation and verification of adherence to specification. Microcontroller memory and step behaviour is specified using a simple imperative language that can be manipulated using standard source code level techniques. This allows cycle-count based deadline checking, simple extension to other microcontrollers in addition to the implemented ATmega328P, and implementation of advanced techniques without dependence on the actual processor used. In addition to the core functionality, advanced techniques for handling nondeterminism, control flow generation, and simple cycle path reduction are implemented. The utility is tested, showing its usefulness for simple program deadline verification. The impact of various techniques used is discussed and promising future improvements are identified.

Formal verification of combined systems of computer programs and physical environment.

Author
Tomáš Zrůst
Year
2015
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Interactive Proof Assistant for Formal Methods Education

Author
Martin Bedrna
Year
2024
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Ing. Jiří Daněček
Summary
This thesis focuses on the implementation of a proof assistant. The inference rules of the proof calculus used by the assistant are a version of natural deduction. In the context of this work, the problem is first introduced theoretically. Subsequently, an analysis and software design are carried out. Finally, the implementation of the created software is described.

Software for the graphical demonstration of quadrocopter motion planning

Author
Tomáš Mahr
Year
2018
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Ing. Lukáš Bařinka
Summary
The goal of this thesis is to design and implement modular software for the graphical demonstration of quadrocopter motion planning. The thesis also explains basic theory of quadrocopter motion planning. One of the existing algorithms is implemented as a module.

Reliable characterization of the existence of solutions of parametric systems of equations

Author
Libor Vytlačil
Year
2018
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
doc. Ing. Ivan Šimeček, Ph.D.
Summary
This thesis deals with the problem of characterizing the sets of points ${p\in P}$, for which there exists a real-valued solution $x$ to a given parametric system of equations $f_P(x,p)=0$, where $f_P\colon X\subseteq\Rsetn{n}\to\Rsetn{n}$ is a continuous function formed by arithmetical expressions and $X$ is a box (product of closed real intervals). A branch and bound like algorithm based on interval arithmetics and a solution existence test using Brouwer's topological degree is designed and implemented. It allows several ways of manipulating the domain $X$ and further parametrization of its operation. Interval arithmetics is used for computing estimates of function images, as well as for providing robustness with respect to rounding errors. The implementation is provided in a form of self-contained application including a user interface (both text-based and graphical). Based on results of the experiments, that are stored in scripts for an easy reproducibility, our implementation is capable of producing quality results and terminate in reasonable time for various non-linear systems up to three equations, possibly containing combinations of elementary functions like $\exp$, $\log$, $\sin$, $\cos$, $\arcsin$, $\arccos$, $n$-th root, $\dots$. We also enhance previous work related to the practical computation of the topological degree by describing and using a custom sound method of determining, if for arbitrary boxes $X'\subseteq X$, $P'\subseteq P$, the degree $\tdeg(f_p, X', 0)$ is defined and has the same value for every $p\in P'$.

Incremental Binary-Decision-Diagram-Based Safety Verification

Author
Vojtěch Hovorka
Year
2013
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Ing. Martin Kohlík, Ph.D.

Library for Orthogonal Polyhedra

Author
Ondřej Šmíd
Year
2016
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Mgr. Jan Starý, Ph.D.
Summary
In this thesis we research representations of orthogonal polyhedra of arbitrary dimension and we research algorithms which include Boolean operations, computing boundary and deciding membership on these polyhedron representations. We implement these representations for polyhedra whose coordinates are floating point numbers.

Handling heap data structures in backward symbolic execution

Author
Robert Husák
Year
2018
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
prof. Ing. Pavel Tvrdík, CSc.
Summary
This thesis enhances AskTheCode, a previously created extension of Microsoft Visual Studio which uses backward symbolic execution to verify assertions in C# code. One of the biggest AskTheCode limitations was the inability to reason about heap objects and operations. In order to implement this feature, we started by surveying existing techniques. As the most promising ones were selected lazy initialization, symbolic initialization and the utilization of the theory of arrays. After an analysis driven by the specific requirements of our tool, we decided to utilize the theory of arrays, mainly due to its expected performance benefits. We transformed the technique to be usable for backward symbolic execution, utilizing assertion stacks of SMT solvers as efficiently as possible. Our solution was proven to be correct by an evaluation on several C# examples.

SAT with differential equations

Author
Tomáš Kolárik
Year
2018
Type
Master thesis
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
doc. RNDr. Pavel Surynek, Ph.D.
Summary
Many nowadays systems, namely embedded, are insisted to satisfy high specification requirements, which often depend on physical features of real world. Formal verification showed to be convenient method to guarantee specifications fulfillment in complex systems. Formal verification checks mathematical model of a system exactly; one of used approaches is e.g. SAT. Problem arises when one needs to use another means of modelling--differential equations (ODEs), which describe physical features natively. Goal of this paper is to prove a concept which combines SAT with ODEs and can be used e.g. to formally verify models of embedded systems. Such solvers already exist (e.g. dReal), but their usage in industry is limited due to their preference of accuracy over speed in ODEs. The objective was to apply classic numerical methods for solving ODEs, which are less accurate, but faster. This work includes prototype implementation named SOS (SMT+ODE Solver), which combines SMT (extension of SAT) with ODEs. SMT and ODE solvers are both independent of rest components. Used solvers are odeint and from SMT solvers CVC4 and z3. The major observations are that using classic numerical methods fastens overall computation, and that computation time of tasks with precise initial values (IVP) is much smaller than at tasks with intervals (IIVP). And intervals can be effectively approximated by value enumerations in logical sum. These observations approve our chosen concept and were verified in some examples, where our procedure was faster than in current solver dReal. Thus the goal of a more appropriate method for industry needs, in the field of formal verification with ODEs, has been reached. This work is assumed to serve as a source of inspiration to industry tools' designers. Or, it can be developing and improving henceforth inside the current open-source project.