Model Checking with Multi-Threaded IC3 Portfolios

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 analysed 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 when on hardware model checking competition examples.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 15, 2015
Accession Number
ADA619756

Entities

People

  • Derrick Karimi
  • Sagar Chaki

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Applied Mechanics
  • Artificial Intelligence
  • Computer Science
  • Computers
  • Data Science
  • Detection
  • Engineering
  • Information Science
  • Knowledge Management
  • Probability
  • Probability Density Functions
  • Random Variables
  • Software Development
  • Statistical Analysis
  • Statistical Distributions

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Distributed Systems and Data Platform Development
  • Enterprise Information Systems Architecture and Joint Command Capability Interoperability Support.
  • Operations Research