|
|||||||||||
 |
|||||||||||
|
| Muri Review Meeting, Nov 30, 2005 | |
| Validation of Control Software |
PPT |
| Verifying
Pointers in Separation Logic |
|
| SAT-based
Predicate Abstraction and Bounded Model Checking |
PPT |
| Efficient
Predicate Abstraction using BDDs |
PPT |
| Dynamic
Component Substitutability Analysis |
PPT |
| Discretization-based
Methods for Timed Verification |
PPT |
| Overview
of Efficient CNF SAT-solving Techniques |
|
| Non-clausal
SAT-solving |
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
Affine-Relation 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 12-13, 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 |
| Wrap-up
for Carnegie Mellon |
PPT |
| Wrap-up
of UW Activities |
PPT |
| Muri Workshop, July 22-23, 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 3-Valued 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 3-valued 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 |