Methods and Algorithms for Analysis of Systems with Infinitely Many States

Standard software development methods, where correctness is checked and guaranteed by a developer (possibly with a small tool support), have reached their limits. At the same time, an undiscovered error in a software system can potentially lead to dramatic financial losses or even to life losses.

This problem can be solved by development of sophisticated tools for automated detection of errors in software system models, or even tools automated or expert-assisted for verification of the systems. In this context, by verification we mean to decide whether a given system satisfies a given specification (more precisely, whether a formal model of the system does not contain a specific type of errors). There is a variety of methods and tools for analysis of formal models with a finite number of states. Unfortunately, such models are not suitable for accurate description of current real systems. The reason is that current systems can be composed of a priori unbounded number of parallel components, they may use recursion, potentially unbounded amount of memory, etc. This is the reason to study the possibilities of infinite-state systems analysis, both on theoretical and practical level.

Main research directions

Information for students

Infinite-state systems analysis is an active and attractive field of research with a direct motivation in software development practice. The area provides many concreate research topics ranging from purely theoretical to as practical as a production of industrial software development tools. We would like to extend our team with bachelor and master students with some programming experience or an ability to pass theoretical courses. The area also offers topics for doctoral study. You can ask an arbitrary team member (either by email or in person) for more information.

Research team members


Department of Computer Science
prof. RNDr. Mojmír Křetínský, CSc.
Phone: +420-549 49 4239