This research addresses the need to increase the reliability of software by continual analysis. One important approach to ensuring system correctness is model checking, in which the verification task is largely automatic and requires minimal user input. Though model checking has been successfully applied in practice, there are a couple of challenges that have limited its applicability. First, the representation of the system that the model checker analyzes is typically very large for most practical systems; this is often called the state space explosion problem. The second is that model checkers analyze a formal model of system which is often unavailable or difficult to construct. In this project, the PI plans to address these challenges by integrating ideas from computational learning theory and randomized algorithms to develop model checking algorithms with provably formal guarantees that can analyze black box systems within available computational resources.
