Explicit-Symbolic Modeling for Formal Verification

November 14, 2007
Sergio Campos | Universidade Federal de Minas Gerais

In this talk we present a model that combines explicit and symbolic representations in an explicit-symbolic model checking tool. Both explicit and symbolic models have been successfully used in the verification of finite state concurrent systems, such as complex sequential circuits and communication protocols. The proposed model aims to use explicit and symbolic techniques together to verify the same model and to make it possible to employ the most efficient technique to each aspect of the model. First, we formalize the explicit-symbolic model and show how it can be generated from a labelled state-transition system.
Then, we apply those ideas to systems described in the Verimag Intermediate Format and present the main algorithms for integrating the underlying models.

Speaker Details

Sérgio V. Campos has received the bachelors degree in computer science from Universidade Federal de Minas Gerais (Belo Horizonte — Brasil) in 1986, the masters degree in computer science from the same university in 1990 and the Ph.D. degree in Computer Science from Carnegie Mellon University in 1996 on the topic of formal verification of real-time systems. During his Ph.D. he has spent two summers working at Intel performing formal verification of hardware circuits.He has spent one year as a post-doctoral researcher at Carnegie Mellon and is currently an associate professor at the computer science department of Universidade Federal de Minas Gerais. While at UFMG Sergio has worked on various topics such as formal verification of hardware and software, the design and implementation of multimedia systems, scheduling problems and telecommunication network management.His interests include design, analysis and verification of real-time systems, hardware and software in general. More recently Sérgio has been the PI of the “Popular PC” project that developed a low cost computer for the use in remote and underdeveloped areas.