VeriFIT: a successful research group. Not just at the Computer-Aided Verification conference

The faculty’s VeriFIT research group, which focuses on automated analysis and verification, has achieved an exceptional publication record. At one of the world’s most prestigious (CORE A*, 25% acceptance rate) conferences in the field of formal methods and verification, Computer Aided Verification (CAV), no fewer than five papers to which members of the group made a significant contribution were accepted. This represents a highly unusual concentration of accepted papers. FIT VUT is thus ranked among the world’s most successful institutions at this year’s CAV conference. No fewer than four of the authors are supported by the international VASSAL project, which is coordinated by our faculty. The global reach of VeriFIT is also evidenced by the fact that three leading researchers from the group – Milan Češka, Lukáš Holík and Ondřej Lengál – are members of the conference’s programme committee.

Reliability of agent-based systems

Broadly speaking, the VeriFIT research group focuses on research into methods of automated analysis and verification of systems, which serve to ensure the reliability and explainability of the execution of computational operations and entire systems. At the same time, it is a diverse group comprising several sub-groups, each with its own research topics. Let’s take a closer look at them.

The first sub-group is led by Associate Professor Milan Češka, who is currently collaborating with three PhD students (Roman Andriushchenko, Filip Macák and David Hudák) and a number of undergraduates. Češka and his colleagues focus on developing methods that enable the automated design of reliable agent-based systems. They are working on methods that allow us to quantify the probability that the resulting system will exhibit the required behaviour. This approach is crucial for systems operating in uncertain environments, such as autonomous control systems, robotics and decision-making systems for economic or healthcare applications.

“Let’s imagine an autonomous car approaching a junction where a child is standing at the pedestrian crossing. Although the car has a green light, it must account for the possibility that the child might step onto the crossing when the light is red, and therefore it must react appropriately – driving smoothly through the junction to ensure that a collision with the child remains highly unlikely, even if the child does step onto the crossing,” says Češka, describing the scope of application for such systems as clearly as possible.

Among the five papers accepted at CAV, two were co-authored by Milan Češka and his colleagues:

• Linus Heck, Filip Macák, Roman Andriushchenko, Milan Češka, Sebastian Junges. Shields to Guarantee Probabilistic Safety in MDPs.
• Milan Češka, Sebastian Junges, Luko van der Maas, Filip Macák, Tim Quatmann. Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families.

Automata

The second strand within the VeriFIT research group is the group led by Associate Professor Lukáš Holík, known as Automata@FIT. Its research lies at the intersection of computer science, logic and mathematics: the group develops theoretical methods based on automata, i.e. finite descriptions of often infinite sets of possibilities – for example, all words, inputs, computations or programme states. This makes it possible to automatically determine the states a programme can reach, whether the programme satisfies the required properties, or where the limits lie of what can still be verified computationally. Formal methods help to uncover errors and security vulnerabilities where conventional testing cannot provide sufficient certainty. One of the group’s key areas of focus is string constraint solving, i.e. the automatic analysis of strings (the string data type) which appear, for example, in web applications, database queries or access policies in the cloud. Such methods can help verify that no input capable of causing an error or a security incident will enter the programme. Another paper accepted at CAV relates to this topic:

• David Chocholatý, Vojtěch Havlena, Juraj Síč, Lukáš Holík, Michal Šedý. String Solving with Stabilisation and Transducers.

Another automata problem studied at VeriFIT involves efficient methods for working with finite-state machines over infinite strings. These automata are often used to model reactive systems, such as operating system components or computer hardware, where correct functionality is critical. Research led by Associate Professor Ondřej Lengál focuses on how to work effectively with these automata, which has applications, for example, in the verification of the aforementioned critical systems.

• O. Alexaj, V. Havlena, L. Holík, O. Lengál, Y. Li, N. Mazzocchi. Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking.

Verification of quantum circuits

The third sub-group within VeriFIT is centred around Associate Professor Ondřej Lengál. It focuses on the intersection of formal methods, automata and quantum technologies – an area that has begun to develop significantly at the faculty in recent years. Lengál is primarily engaged in the verification and simulation of quantum programmes. In collaboration with researchers from Taiwan, he is working on methods and tools designed to support the design of quantum programmes and to help verify that quantum programmes actually do what we expect them to do. The latest article accepted by CAV relates to this topic:

• W. Tsai, Y. Chen, O. Lengál. A Practical Specification Language for Automatic Quantum Program Verification.

VeriFIT is one of the driving forces behind specialist research at the Faculty of Information Technology and plays a significant role in ensuring that our faculty ranks among the leading university research organisations in the Czech Republic. We would like to thank its members and wish them plenty of perseverance and further success in the near future.

Zdroj: FIT BUT

Themes

Related articles:
A student at FIT on internship in CERN develops software that controls particle accelerators
We haven't reached worst point yet. Interview with Anton Firc, Joseph Fourier Prize awardee
BUT sensors protect bee colonies from starvation and theft
LECTURE AS A STORY WITH A PLOT, DENOUEMENT AND LESSON
A different way to collect stamps. FIT BUT students are developing a digital benefit app