• Parallelizing Irregular Applications
• Lonestar Benchmark Suite

• Compiling for Distributed Memory Computers
• Control Dependence Computation
• Empirical Optimization
• Fault Tolerance
• Fractal Symbolic Analysis
• Functional Languages with Logic Variables
• Memory Hierarchy Optimizations
• Model Checking for Hierarchical State Machines
• Program Representation
• Static Single Assignment Form
• Synthesis of Irregular Codes
• Web Services for Distributed Scientific Computing

Model Checking for Hierarchical State Machines

"... a xenomorph may be involved."
-- Lt. Gorman, Aliens (1986)

Model Checking refers to a collection of techniques for determining the validity of a temporal logic expression over a structure, usually some variety of graph. Applied to software, model checking is an approach in which properties (desirable or undesirable) of a program are encapsulated as logical formulas and then validated against an abstract representation of a program. As a simple example, if one wanted to ensure that there was no path in a program in which a function "foo" was called before a function "bar", a logical formula to encapsulate that could be expressed in computation tree logic (CTL) as A [bar R ~foo]. In English, this formula asserts that on all program paths a call to "bar" releases the condition that there is not a call to foo. If this formula is valid over a control flow graph of a program then the desired property holds. The goal of software model checking is then to devise formulas and models that allow conclusions to be drawn about the behavior of the program being considered.

Our research focuses on a particular type of model, the hierarchical state machine (HSM). This class of model is powerful enough to encapsulate the call and return structure inherent in imperative programs. Within the framework of these models we focus on:

• Context-sensitive algorithms and optimizing techniques for validating temporal logic formulas over HSMs
• Techniques for simplifying large batches of formulas
• Generation of space efficient models for specified program properties
• Practical source level counter-example generation
• Techniques for specifying high-level design and usage constraints in formal language

The practical applications of this work include:

• Finding bugs in code
• Proving the correctness of code
• Making existing code instantly accessible to newly assigned programmers

Project Participants:

• James Ezick

Contributors:

• GrammaTech, Inc. (Our software is a plug-in to their CodeSurfer program analysis tool.)

Publications:

• James Ezick An End-to-End System for Model Checking over Context-Sensitive Analyses Cornell Computer Science PhD Thesis, 08/01/2004
• James Ezick An Optimizing Compiler for Batches of Temporal Logic Formulas International Symposium on Software Testing and Analysis, 07/12/2004
• James Ezick Resolving and Applying Constraint Queries over Context-Sensitive Analyses Workshop on Program Analysis for Software Tools and Engineering, 06/07/2004
• James Ezick Resolving Constrained Existential Queries over Context-Sensitive Analyses Cornell University Computing and Information Science Technical Report TR2003-1913, 06/04/2003