Alessandro Cimatti wins ETAPS “Test of Time Award”

In an ever-changing and fast-moving field like software is, not everybody gets to make an internationally ground-breaking and far-reaching scientific work that will influence the industry for years to come.

Alessandro Cimatti, with Fondazione Bruno Kessler‘s ICT Center, has succeeded: he received yesterday in in Upspsala, Sweden, the “Test of Time Award” from ETAPS, the joint European conferences on theory and practice of software.

His scientific work “Symbolic model-checking without BDDs” carried out in 1999 with Prof. Edmund Clarke‘s group at Carnegie Mellon University has been selected among the over 1,000 published in ETAPS conferences until 2007, the period considered for this year’s selection, and awarded the prize dedicated to articles that have withstood the test of time.

The study involved the implementation of the so-called Bounded Model Checking, an algorithm that is now used in all electronic circuit and software design systems. In particular, it is used to automatically check for design errors – before the circuit itself is produced – so that they can be corrected in time, ensuring faster speed and money savings. To prove the big influence it has had, the original article and its later evolutions have so far been cited more than 3,800 times in scientific works in its field.

“Often,” Cimatti says, “we obtain amazing results by combining ideas from various disciplines. The work, inspired by Artificial Intelligence, in particular by Planning, has produced a highly innovative technique in digital systems verification. Bounded Model Checking has paved the way for program and circuit analysis that was simply out of the reach of the techniques available at that time. ”

Cimatti, who has recently received his Full Professor certification in Computer Science and Information Processing Systems, has been the Head of the Embedded Systems (ES) Research Unit in the ICT Center of Fondazione Bruno Kessler since 2007.

The Unit develops various kinds of software for formal verification where Bounded Model Checking is an integral part. Formal verification is applied to multiple technology transfer projects in critical areas such as aerospace, railway, advanced control, and Industry 4.0.