Sagar Chaki

Sagar Chaki, Derrick Karimi, Proceedings of the 17th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), January 17--19, 2016.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

Abstract:Three variants of multi-threaded IC3 are presented. Each variant has a fixed number of IC3s running in parallel, and communicating by sharing lemmas. They differ in the degree of synchronization between threads, and the aggressiveness with which proofs are checked. The correctness of all three variants is shown. The variants have unpredictable runtime. On the same input, the time to find the solution over different runs varies randomly depending on the thread interleaving. The use of a portfolio of solvers to maximize the likelihood of a quick solution is investigated. Using the Extreme Value theorem, the runtime of each variant, as well as their portfolios is analyzed statistically. A formula for the portfolio size needed to achieve a verification time with high probability is derived, and validated empirically. Using a portfolio of 20 parallel IC3s, speedups over 300 are observed compared to the sequential IC3 on hardware model checking competition examples. The use of parameter sweeping to implement a solver that performs well over a wide range of problems with unknown "hardness" is investigated.