Alessandro Cimatti and Roberto Sebastiani win the Computer-Aided Verification Award 2021

The recognition was awarded for their pioneering research in the field of SMT (“Satisfiability Modulo Theories”), an Artificial Intelligence discipline that aims to develop algorithms capable of automatically solving logical-mathematical problems and which has as its main application the correct design  of microprocessors, software and highly critical systems. In short, it involves designing computer systems that verify the correctness of other computer systems, which are used, for example, in the verification of the control and safety systems of vehicles such as airplanes and hardware devices.

The award, won together with other globally renowned authors, was announced during the conference whose edition this year was organized as an online event due to the current pandemic crisis. The official awards ceremony will take place during the 2022 edition which will be held in Israel.

Alessandro Cimatti, director of the Center for Digital Industry at Fondazione Bruno Kessler, has received the prestigious award for the second time, after being awarded it at the 2018 edition. Roberto Sebastiani, full professor with the Department of Information Engineering and Computer Science (DISI) at the University of Trento, is the author of one of the most cited papers on SMT in the world. They have collaborated for over twenty years: together they have written nearly forty scientific articles, many of which are foundational works on the subject for which they have been awarded; they have created the MathSAT project, and supervised many PhD students jointly. One of their papers on a project for the application of SMT to the verification of microprocessors for Intel was awarded at the conference “Formal Methods for Computer-Aided Design” in 2010.

“SMT-based techniques”, said Alessandro Cimatti, “have become one of the technology pillars of the Center for Digital Industry, which is at the forefront of formal verification and safety analysis, with numerous technology transfer projects in the avionics, space, railway, electronics and process control fields”.

“SMT”, Roberto Sebastiani pointed out, “originated from the intuition  to integrate algorithms for logical reasoning with others belonging to very different fields, such as the numerical solution of mathematical problems or the manipulation of character or element sequences, would increase their effectiveness and considerably expand their fields of application.”