OREGON STATE UNIVERSITY

You are here

Bounded Model Checking and Feature Omission Diversity

TitleBounded Model Checking and Feature Omission Diversity
Publication TypeConference Paper
Year of Publication2011
AuthorsAlipour, A., and A. Groce
Conference NameSeventh International Workshop on Constraints in Formal Verification
Date Published11/2011
Conference LocationSan Jose, California
Abstract

In this paper we introduce a novel way to speed up the discovery of counterexamples in bounded model checking, based on parallel runs over versions of a system in which features have been randomly disabled. As shown in previous work, adding constraints to a bounded model checking problem can reduce the size of the verification problem and dramatically decrease the time required to find counterexample. Adapting a technique developed in software testing to this problem provides a simple way to produce useful partial verification problems, with a resulting decrease in average time until a counterexample is produced. If no counterexample is found, partial verification results can also be useful in practice.