|
Change #9162
2011-07-05
10:48:42
|
create
Calagator::Event
1250460798
Galois tech talk: Parallel K-induction based Model Checking
Roll back
| description |
nil |
→ |
Presented by Temesghen Kahsai.
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. |
| end_time |
nil |
→ |
2011-07-12 11:30:00 -0700 |
| id |
nil |
→ |
1250460798 |
| start_time |
nil |
→ |
2011-07-12 10:30:00 -0700 |
| title |
nil |
→ |
Galois tech talk: Parallel K-induction based Model Checking |
| url |
nil |
→ |
http://corp.galois.com/blog/2011/7/5/tech-talk-parallel-k-induction-based-model-checking.html |
| venue_id |
nil |
→ |
202390439 |
|