You are here

The "most influential paper in the first 20 years of TACAS" prize awarded to Alessandro Cimatti

News date: 
Thursday, 10 April, 2014

Thanks to the 1797 citations (up to December 2013), it proved to be the most quoted paper in the long history of the TACAS (Tools and Algorithms for the Construction and Analysis of Systems) Conference, the international event that gathers scholars in the field of formal methods for the design of correct digital systems for construction.During the 20th edition, that was held in Grenoble, France a past few days, FBK researcher Alessandro Cimatti received the prestigious award for his article"Symbolic Model Checking without BDDs", written with Armin Biere, Edmund M. Clarke and Yunshan Zhu. The paper introduces an innovative checking technique, called Bounded Model Checking: it is the first technique based on an efficient use of SAT solvers ("Boolean satisfiability") and oriented to error detection.Following the publication of the article, in 1999, this particular technique was actually adopted by all industrial systems of formal checking.The news of the award was also reported on "ETAPS 2014 DAILY", the news bulletin of the Grenoble 2014 conference.