Galois is pleased to host the following tech talk.
These talks are open to the interested public. Please join us!
title:
Parallel K-induction based Model Checking
speakers:
Temesghen Kahsai
time:
Tuesday, 12 July 2011, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
We give an overview of a parallel k-induction-based model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. A first level of parallelism is introduced in the k-induction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the k-induction loop as soon as they are produced and used to strengthen the induction hypothesis.
This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property — valid or invalid — is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties.
We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties.
bio:
Temesghen Kahsai is a postdoc research scholar at the University of Iowa. He recevied a BSc and an MSc in Computer Science from the University of Udine (Italy) and a Ph.D. in Computer Science from Swansea University (Wales). His research interests include formal specification languages, software verification, specification-based testing and interactive theorem proving. Currently, he is working on SMT-based model checking for synchrouns systems. His publications and other information can be found at www.cs.uiowa.edu/~tkahsaiazene