Software Engineering Institute

This paper appeared in the Proceedings of the 17th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), January 2016, pp. 517-535.

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 its 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.