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.
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).
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.
The conference hotel is a Holiday Inn in downtown Baltimore, Maryland. A special booking rate is available to conference attendees.
This page modified November 20, 2003.