2007.04.11 | Doina Bucur

Title: Verification with Bounded Model Checking
Speaker: Keijo Heljanko (Academy Research Fellow, Helsinki University of Technology)

Abstract:

Model checkingis a set of methods for analysing whether a model of
a system (e.g., a Petri net) fulfils its specification given as
a temporal logic formula. Bounded model checking (BMC) was introduced
by Biere et. al to further improve the scalability of model checking by
applying methods based on propositional satisfiability (SAT). In bounded
model checking only counterexample executions of the system that are
shorter than some fixed length are considered. The success of BMC,
especially in the context of hardware verification, is based on the
enormous advances in SAT solving techniques achieved during the last
few years. In this talk we focus is on topics which arise when creating
an efficient bounded model checkers for an asynchronous system model
(e.g., a 1-bounded Petri net). This requires the use of efficient SAT
encodings for the model checking problem at hand.

Speaker's bio:

Keijo Heljanko is an Academy Research Fellow working at Laboratory for
Theoretical Computer Science, Helsinki University of Technology (TKK).
His research interests are in the areas of computer aided verification
tools and algorithms, distributed systems, model checking, and
net unfoldings. Keijo received his Master's and doctoral degrees from TKK,
and worked as a PostDoc with Prof. Javier Esparza in Stuttgart, Germany
before returning back to TKK. More information about him can be found
on hiswebpage (http://www.tcs.tkk.fi/~kepa/).