Verifying next-generation hardware and software systems
FBK researcher Silvio Ranise was awarded the “HVC Award” (Haifa Verification Conference)
(m.l.) The protection and security of personal data is one of the most pressing issues for hardware and software system design companies. A simple oversight or a “worm” can become a tempting target for viruses and IT pirates. Reliability is a fundamental requirement for preventing disservices and system malfunctioning. This is the context of the research by Silvio Ranise of the “Security and Trust” unit of the Information Technology Center of Fondazione Bruno Kessler in Trento, who recently received the international “HVC Award”.
Ranise shared this prestigious recognition with four other researchers belonging to a number of American organizations. Further, Ranise was also honoured with “the most promising contribution in the past five years in hardware and software verification.” Specifically, the “HVC Award” was presented to Silvio Ranise in 2010 “for the key role played in building and promoting the SMT (Satisfiability Modulo Theories) community”. In fact, Silvio Ranise not only contributed to founding this scientific community, he developed a number of key techniques and studied their most important applications.
Formerly a researcher at the INRIA (Institut National de Recherche en Informatique et en Automatique, France), Ranise has been working at the “Security and Trust” research unit of the IT Center of the FBK since April 2010, guided by professor Alessandro Armando. Ranise is expanding his research in application of SMT techniques to IT system security analyses as part of a research project of the VII Framework Programme, financed by the Autonomous Province of Trento.
Multinationals such as Microsoft and Intel, to name just two examples, use SMT-based verification tools to design their products. What are “SMT” (Satisfiability Modulo Theories) techniques?
The acronym “SMT” denotes a set of techniques used in solving the logical and mathematical problems that underlie next-generation software and hardware verification tools. These tools are fundamentally important for those who design IT systems increasingly present in people’s everyday lives. These systems, used in areas in which their reliability is vitally important, become more complex and sophisticated each day, eluding the analytical abilities of even the most skilled designers. The widespread use of SMT techniques, which represent the basis for developing verification tools for large-scale systems, began in 2003 and interest in it by both the international scientific community, with a growing number of publications, and by global industry has multiplied since then.
The “HVC” conference (Haifa Verification Conference)
Since 2005, the “HVC” (Haifa Verification Conference) has been held annually in Haifa (Israel) and is sponsored by IBM. At this event, participants can meet experts in the field of IT system verification from every part of the world. The “HVC Award” was instituted in 2007 and is awarded to researchers who make a significant contribution in the form of scientific articles, systems or activities focused on developing hardware and software system verification techniques.