Thomas Ball
Microsoft Research, USA
"A Theory of Predicate-Complete Test Coverage and Generation"
Patrick Cousot École
Normale Supérieure, FR
"Automatic Verification of Infinite-State Systems by Abstract Interpretation"
Cathy Meadows Naval Research Laboratory,
USA "Formal Methods for Cryptographic Protocol
Analysis: Emerging Issues and Trends"
Thomas Reps
University of Wisconsin, USA
"Weighted Pushdown Systems and their Applications"
Scott Stoller
SUNY at Stony Brook, USA
"Towards Automated Verification of Software Through Type Discovery"
| Time |
Saturday, 3rd April 2004
|
| 0845
- 0900 |
Welcome
and Introduction (AVIS organizers) |
| 0900
- 1000 |
Invited
Talk I: A Theory of Predicate-Complete Test Coverage and
Generation
Thomas Ball (Microsoft
Research, USA) |
| 1000
- 1030 |
Coffee
break |
| 1030
- 1130 |
Invited
Talk II: Automatic Verification of Infinite-State Systems by Abstract
Interpretation
Patrick Cousot
(École Normale Supérieure,
FR) |
| 1130
- 1230 |
Paper
Session I - Behavioral Equivalence Checking
11.30: On the Application of Counterexample-Guided
Abstraction Refinement and Data Independence
to the Parameterised Model Checking Problem
G. Lowe (Oxford University Computing Laboratory, UK)
12:00: Bisimilarity on Normed Basic
Parallel Processes can be decided in time O(n3)
Peter Jancar and Martin Kot (Technical University of Ostrava, CZ) |
| 1230
- 1400 |
Lunch |
| 1400
- 1500 |
Invited
Talk III: Weighted Pushdown Systems and their Applications
Thomas Reps (University
of Wisconsin, USA) |
| 1500
- 1600 |
Paper
Session II: Static Analysis
15.00: State Space Abstraction using
Shape Graphs
Arend Rensink (University of Twente, NL)
15.30: Towards Symbolic Verification
of Programs Handling Pointers
Sébastin Bardin, Alain Finkel, and David Nowak (LSV, ENS Cachan,
and CNRS UMR, FR) |
| 1600
- 1630 |
Coffee
break |
| 1630
- 1730 |
Invited
Panel: The Future of Software Verification
Moderator: Ramesh
Bharadwaj
Panelists:
Tom Ball
Patrick Cousot
Connie Heitmeyer
Tom Reps |
| Time |
Sunday, 4th April 2004
|
| 0900
- 1000 |
Invited
Talk IV: Towards Automated Verification of Software Through Type
Discovery
Scott D. Stoller
(State University of New York at Stony Brook, USA) |
| 1000
- 1030 |
Coffee
break |
| 1030
- 1130 |
Paper
Session III: Verification of Asynchronous Systems
10.30: Verifying Nondeterministic Channel
Systems with Probabilistic Message Losses
N. Bertrand and Ph. Schnoebelen (ENS de Cachan and CNRS UMR, FR)
11:00: Verification of Asynchronous
Systems with Unbounded and Unordered Message Buffers
Prasanna Thati and Mahesh Viswanathan (University of Illinois, USA) |
| 1130
- 1230 |
Invited
Talk V: Formal Methods for Cryptographic Protocol Analysis: Emerging
Issues and Trends
Catherine Meadows
(Naval Research Laboratory, USA) |
| 1230
- 1400 |
Lunch |
| 1400
- 1500 |
Paper
Session IV: Security Protocol Verification
14.00: Improvements on the Genet and Klay
Technique to Automatically Verify Security Protocols
Y. Boichut, P.-C. Héam, O. Kouchnarenko and F. Oehl (INRIA CASSIS,
FR and Dublin City University, IE)
14.30: A Proof of Correctness for Cryptographic
Key-agreement Protocols using Event-recording Automata
Suman Roy (Honeywell Technologies, IN) |
| 1500
- 1530 |
Final discussion and closing
remarks |