With recent advances in algorithms for state-space traversal and in techniques for automatic abstraction of source code, model checking has emerged as a key tool for analyzing and debugging software systems. This proposal is centered around the role of games in modeling and analysis of software systems. Games are useful in modeling open systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. The first thrust of this research will investigate application of games for component-based design and modular verification. It will explore how games can be used to generate abstractions that capture the most general environment assumptions needed to satisfy requirements, and as dynamic types for interfaces. The second thrust will address the challenge of scalability in presence of high computational complexity of the analysis problems. Symbolic techniques and heuristics for solving games with partial information will be developed using satisfiability solvers and packages for manipulating binary decision diagrams. These techniques will be implemented and and applied to case studies in domains such as network protocols, device drivers, and medical devices.
