


Muri Review Meeting, Nov 30, 2005  
Validation of Control Software 
PPT 
Verifying
Pointers in Separation Logic 

SATbased
Predicate Abstraction and Bounded Model Checking 
PPT 
Efficient
Predicate Abstraction using BDDs 
PPT 
Dynamic
Component Substitutability Analysis 
PPT 
Discretizationbased
Methods for Timed Verification 
PPT 
Overview
of Efficient CNF SATsolving Techniques 

Nonclausal
SATsolving 
PPT 
Muri Review Meeting, Feb 15, 2005  
Introduction 
PPT 
Verification
of Embedded Systems 
PPT 
Extending
MAGIC with Recursion 
PPT 
Applied
Software Model Checking 
PPT 
From
Model Checking to Proof Carrying Code 
PPT 
Verifying
Component Substitutability 
PPT 
Overview
of UW Activities 
PPT 
Inductive
Logic Programming for Learning Abstractions 
PPT 
A
Framework for Numeric Analysis of Array Operations 
PPT 
Improving
AffineRelation Analysis in x86 code 
PPT 
Muri Review Meeting, Aug 16, 2004  
CBMC and C Model Checking 
PPT 
Automated
Compositional and Iterative Deadlock detection 
PPT 
Extending
MAGIC with Recursion 
PPT 
Verifying
Component Substitutability 
PPT 
Overview
of UW Activities 
PPT 
Muri Review Meeting, Nov 1213, 2003  
Static Analysis to Enhance the Power of
Model Checking for
Concurrent Software 
PPT 
Assuring
Software Quality by Model Checking 
PPT 
Overview
of UW Activities 
PPT 
The
MAGIC Project: Verification of C Components 
PPT 
Shape
Analysis 
PPT 
Verification
of Embedded Systems 
PPT 
Weighted
Pushdown Systems 
PPT 
Wrapup
for Carnegie Mellon 
PPT 
Wrapup
of UW Activities 
PPT 
Muri Workshop, July 2223, 2003  
Assuring
Software
Quality UW Overview 
PPT 
Trust
Management
via Weighted Pushdown Systems 
PPT 
Creating
General
Version of Java Procedures 
PPT 
Automatic
Abstraction Refinement for 3Valued Logic Analysis 
PPT 
New
Approach to
Abstraction of Numeric Quantities 
PPT 
Explaining
Errors 
PPT 
Modular
Verification of Software Components in C 
PPT 
Symbolic
Model
Checking of Software 
PPT 
Other presentations can be found at the Review meeting website 
Muri Workshop, December 2002  
Conformance
checking for Concurrent C Programs 
PPT 
Minimum
Simulation
Proofs 
PPT 
SAT
based
Predicate Abstraction 

Overview
 WISA 
PPT 
Symbolic
Implementation of the Best Transformer 
PPT 
Finite
Differencing of Logical Formulas for Static Analysis 
PPT 
Verifying
Behavioral Subtyping 
PPT 
Muri Workshop, January 2002  
Program
analysis
via 3valued logic 
PPT 
Towards
abstraction refinement in TVLA 
PPT 
A
propositional
world 
PPT 
Verifying
regular
behavior of C modules 
PPT 
Other Presentations  
Conformance
Checking for Software 
PPT 
Model
Checking of
Concurrent Software: Current Projects 
PPT 