CMU logo Wisconsin logo

Muri Review Meeting, Nov 30, 2005
Validation of Control Software
Flavio Lerda, CMU
Verifying Pointers in Separation Logic
Stephen Magill, CMU
SAT-based Predicate Abstraction and Bounded Model Checking
Himanshu Jain, CMU
Efficient Predicate Abstraction using BDDs
Constantinos Bartzis, CMU
Dynamic Component Substitutability Analysis
Nishant Sinha, CMU
Discretization-based Methods for Timed Verification
Muralidhar Talupur, CMU
Overview of Efficient CNF SAT-solving Techniques
Tamir Heyman, CMU
Non-clausal SAT-solving
Constantinos Bartzis, CMU

Muri Review Meeting, Feb 15, 2005
Introduction
Ed Clarke, CMU
Verification of Embedded Systems
Daniel Kroening, CMU
Extending MAGIC with Recursion
Constantinos Bartzis, CMU
Applied Software Model Checking
Dan Milam, CMU
From Model Checking to Proof Carrying Code
Aleksandar Nanevski, CMU
Verifying Component Substitutability
Nishant Sinha, CMU
Overview of UW Activities
Thomas Reps, UW
Inductive Logic Programming for Learning Abstractions
Alexey Loginov, UW
A Framework for Numeric Analysis of Array Operations
Denis Gopan, UW
Improving Affine-Relation Analysis in x86 code
Akash Lal, UW


Muri Review Meeting, Aug 16, 2004
CBMC and C Model Checking
Alex Groce, CMU
Automated Compositional and Iterative Deadlock detection
Sagar Chaki, CMU
Extending MAGIC with Recursion
Tayssir Touili, CMU
Verifying Component Substitutability
Nishant Sinha, CMU
Overview of UW Activities
Thomas Reps, UW
Muri Review Meeting, Nov 12-13, 2003
Static Analysis to Enhance the Power of Model Checking for Concurrent Software
Edmund Clarke, CMU
Assuring Software Quality by Model Checking
Edmund Clarke, CMU
Overview of UW Activities
Thomas Reps, UW
The MAGIC Project: Verification of C Components
Sagar Chaki, CMU
Shape Analysis
Thomas Reps, UW
Verification of Embedded Systems
Daniel Kroening, CMU
Weighted Pushdown Systems
Thomas Reps, UW
Wrap-up for Carnegie Mellon
Edmund Clarke, CMU
Wrap-up of UW Activities
Thomas Reps, UW

 

Muri Workshop, July 22-23, 2003
Assuring Software Quality UW Overview
Thomas Reps, UW
Trust Management via Weighted Pushdown Systems
Thomas Reps, UW
Creating General Version of Java Procedures
Mulhern, UW
Automatic Abstraction Refinement for 3-Valued Logic Analysis
Alexey Loginov, UW
New Approach to Abstraction of Numeric Quantities
Denis Gopan, UW
Explaining Errors
Alex Groce, CMU
Modular Verification of Software Components in C
Sagar Chaki, CMU
Symbolic Model Checking of Software
Nishant Sinha, CMU
Other presentations can be found at the Review meeting website


Muri Workshop, December 2002
Conformance checking for Concurrent C Programs
Sagar Chaki
Minimum Simulation Proofs
Ofer Strichman
SAT based Predicate Abstraction
Muralidhar Talupur
Overview -- WISA
Tom Reps
Symbolic Implementation of the Best Transformer
Tom Reps
Finite Differencing of Logical Formulas for Static Analysis
Alexey Loginov
Verifying Behavioral Subtyping
Mulhern
Muri Workshop, January 2002
Program analysis via 3-valued logic
Tom Reps
Towards abstraction refinement in TVLA
Alexey Loginov
A propositional world
Ofer Strichman
Verifying regular behavior of C modules
Sagar Chaki
Other Presentations
Conformance Checking for Software
Sagar Chaki
Model Checking of Concurrent Software: Current Projects
Tom Reps