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

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:

• http://www.cs.cas.cz/~ratschan/theses/en/constraint_solving.html

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.

Assume a certain task for a robot, for example: Move from point A to point B without colliding with any obstacle. Robot motion planning is the problem of finding a plan for the actuators of the robot such that the resulting movement of the robot satisfies the given task. The currently dominant class of algorithms for motion planning are sampling based, rapidly expanding a tree that explores the search space of possible plans. However, such algorithms usually use rough approximations the dynamics of the robotics, which may result in highly sub-optimal plans.

The goal of this topic is to design theory, algorithms, and software for efficiently handling realistic models of robot dynamics in sampling based motion planning. All algorithms will be implemented in the frame of the Open Motion Planning Library (OMPL, https://ompl.kavrakilab.org/ ) which will allow their usage by practitioners in robotics world-wide.

Literature: Andreas Orthey, Constantinos Chamzas, and Lydia E. Kavraki: Sampling-Based Motion

Planning: A Comparative Review, Annual Review of Control, Robotics, and Autonomous Systems,Volume 7, 2024

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:

• http://www.cs.cas.cz/~ratschan/theses/cz/verification.html

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

prof. Ing. Róbert Lórencz, CSc.

Department of Theoretical Computer Science

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.

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

doc. Ing. Ivan Šimeček, Ph.D.

Department of Theoretical Computer Science

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.

Thesis on DSpace

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

Mgr. Jan Starý, Ph.D.

Department of Theoretical Computer Science

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.

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

Ing. Josef Vogel, CSc.

Department of Software Engineering

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.

Thesis on DSpace

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

Ing. Martin Kohlík, Ph.D.

Department of Digital Design

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

Department of Software Engineering

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

Mgr. Jan Starý, Ph.D.

Department of Theoretical Computer Science

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.

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

Ing. Lukáš Bařinka

Department of Software Engineering

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.

Thesis on DSpace

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

doc. Ing. Ivan Šimeček, Ph.D.

Department of Theoretical Computer Science

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'$.

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

prof. Ing. Pavel Tvrdík, CSc.

Department of Software Engineering

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.

Thesis on DSpace

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

doc. RNDr. Pavel Surynek, Ph.D.

Department of Digital Design

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.

Thesis on DSpace

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

doc. Ing. Jan Schmidt, Ph.D.

Department of Digital Design

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.

Thesis on DSpace

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

Ing. Jiří Daněček

Department of Software Engineering

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.

Thesis on DSpace