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.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Application #
0448178
Program Officer
Sol J. Greenspan
Project Start
Project End
Budget Start
2005-05-15
Budget End
2011-04-30
Support Year
Fiscal Year
2004
Total Cost
$400,000
Indirect Cost
Name
University of Illinois Urbana-Champaign
Department
Type
DUNS #
City
Champaign
State
IL
Country
United States
Zip Code
61820