News

The article entitled An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits, to which Ondřej Lengál from the VeriFIT group made a significant contribution, was selected as a research highlight for the journal Communications of the ACM. The research highlights section usually selects several of the most interesting results from tens of thousands of articles submitted annually to ACM conferences across all areas of computer science. This is the first time that an article with a Czech affiliation has received this honor. It should be added that the full version of the text was first published in 2023 at the leading PLDI'23 (CORE A*) conference, where it received the Distinguished Paper award.

Developments in the field of quantum computing are advancing inexorably, both in terms of technology (better hardware) and algorithms (better error correction techniques). Quantum computing promises to solve problems that we are currently unable to deal with effectively using conventional techniques, such as factoring large numbers, searching unstructured databases, or problems in the fields of materials engineering, pharmacology, or the simulation of physical systems. However, writing programs for quantum computers is much more demanding than for classical computers—one reason being that quantum programs are probabilistic in nature and the key technique by which they achieve their efficiency is the use of superposition and constructive interference. This can be simplified by imagining that a program runs in several states at the same time, each with a certain probability, and these probabilities can interact with each other: they can amplify or weaken each other. In order to limit the possibility of errors when programming quantum computers, we need tools that can search for errors in quantum programs. However, analyzing quantum programs is a challenging problem even for computers themselves, because a quantum program can be in a superposition of an exponential number of states at any given moment, all of which must be taken into account during analysis.

The article introduces a new approach to the automatic verification of quantum computations using automata theory and builds a bridge between these two research areas (quantum computing and automata). Automata (specifically finite tree automata, which are an extension of standard finite automata representing regular languages) are used here for the compact representation of complex sets of quantum states. Follow-up work introduces variants of these automata that allow the representation of sets of quantum states with several dimensions of infinity (such as the number of qubits or potential amplitude values) and the verification of parametric quantum programs (e.g., that the algorithm works correctly for any number of qubits).

The article was written in collaboration with researchers from Academia Sinica in Taiwan (Republic of China), with whom the VeriFIT group has been actively collaborating for more than 15 years. The text of the article is available HERE.

A recording of Ondřej Lengál's public habilitation lecture on the topic is also available.

As is tradition, in the week before classes begin, specifically from Thursday, September 11 to Sunday, September 14, our faculty hosts an important introductory activity for first-year students called Start@FIT. The event is organized and sponsored by the FIT VUT Student Union. It is designed to help new students take their first steps in university life, introduce them to the faculty, and offer them the opportunity to get to know their classmates, teachers, and Brno itself.

Participants can look forward to practical content covering topics such as:

• How to create a schedule and register for courses/exercises
• IS VUT
• Orientation on the faculty campus
• ... and, of course, the matriculation ceremony

More detailed information about the program and a handbook for first-year students are available HERE.

650 years ago, on August 13, 1375, Margrave John Henry of the House of Luxembourg issued the founding charter of the Carthusian monastery "Cella Trinitatis". This marked the birth of a complex that is now a historical landmark in the Královo Pole district of Brno. It is also a place where history meets state-of-the-art information technology.

The monastery was originally founded for a prior and 12 monks, so it included 12 cells for Carthusian fathers. The strict rules of coexistence of the monks of the Carthusian order, inspired by hermit ideals, were also reflected in the architectural elements. The individual cells were accessible from separate monastic gardens, towards which the windows of the cells also faced, thus preventing contact between the monks.

The monastery was repeatedly affected by war events. It was damaged during the Hussite and Czech-Hungarian wars, and suffered particularly during the Thirty Years' War. Nevertheless, it experienced a period of economic growth after the mid-18th century. Subsequently, however, it fell victim to the reforms of Joseph II, like many other church buildings in our country. The complex was turned into barracks. The military use of the complex continued until 1964, when the Czechoslovak People's Army handed it over to the Czech Technical University. Paradoxically, it was precisely the military use that helped to preserve the building and its historical value. That is why we now have before us a valuable example of a typical medieval charterhouse with subsequent Baroque modifications. The complex was given a new lease of life by renovations begun at the start of the 21st century based on a design by architect Vladislav Vrána.

Let us appreciate the places and legacies that we can pass through every day. More information about the history of the monastery and a gallery of historical images can be found HERE.