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 cs.uiowa.edu/~tkahsaiazene