However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs -- even those with a single unbounded integer. A second problem is that of state-space explosion, i.e., the exponential blow-up suffered when systems have large numbers of variables and concurrent components.
In this talk, I will address our progress on these problems. First, I will outline our integer-based model-checker, which uses linear constraints and logical connectives in its underlying state representation. With this model, we compactly represent huge (even unbounded) sets of integer states in multiple dimensions. Next, I will present our composite analyzer, which combines the strengths of both BDDs (for Boolean and enumerated types), and linear constraints (for integers). Using this technique, a system's states are encoded via both representations, where the choice depends on the variable types. In essence, type-specific symbolic encodings are unified into one composite model-checker. I will also show how we use composite model-checking in concert with some conservative approximation methods; and how the result provides a solid framework for our investigations in large problem domains.
Finally, I will discuss how we used these methods to automatically analyze some subtle, nontrivial infinite-state systems -- the type of systems usually analyzed by hand (or via on-line testing). Specifically, I will discuss our experiments from domains such as requirements engineering, protocol analysis, and concurrency control.
Biography
Tevfik Bultan is a Ph.D. candidate at the Department of Computer
Science at the University of Maryland, College Park. He received the B.S.
degree in electrical engineering from the Middle East Technical University,
and the M.S. degree in computer engineering and information sciences from
the Bilkent University, both in Ankara, Turkey. His current research interests
are in automated tool-support for design and analysis of concurrent systems,
formal methods, requirements engineering, computer-aided verification,
and automated testing/debugging methodologies.