MURI Review Meeting
November 12-13, 2003
Baltimore, Maryland

Meeting Home || Agenda || Registration || Hotel

Static Analysis to Enhance the Power of Model Checking for Concurrent Software

Edmund Clarke, Thomas Reps, and Somesh Jha

The CMU-Wisconsin software model checking project employs methods from both static analysis and model checking to verify properties of software. In particular, we employ static analysis as a tool to construct abstract models on which model checking will be subsequently performed.

Project web site

Vulnerability and Information Flow Analysis of COTS

Somesh Jha, Barton Miller, and Thomas Reps

We develop analysis techniques especially suited for commercial off-the-shelf components. We combine techniques from static analysis (such as program slicing, shape analysis, and alias analysis), model checking (such as rely-guarantee reasoning), specifications for security policy expression (such as security automata), and formalisms for expressing information flow (such as secure flow typing and decentralized labels).

Project web site

These projects are sponsored by the Office of Naval Research under the Critical Infrastructure Protection and High Confidence, Adaptable Software Research Program of the URI.


An online agenda is available.


Online registration is closed.

Hotel Information

The conference hotel is a Holiday Inn in downtown Baltimore, Maryland. A special booking rate is available to conference attendees.

Meeting Home || Agenda || Registration || Hotel

This page modified November 20, 2003.