July 6, 1999 - Room 7-L |
 |
|
| 8:45 - 9:00
|
|
Introduction to
the workshop |
|
|
|
| 9:00 - 10:00 |
|
INVITED TALK
Translation Validation
Amir Pnueli (Weizmann Institute of Science) |
|
|
|
| 10:00 - 10:30 |
|
COFFEE BREAK |
|
|
|
| 10:30 - 11:00 |
|
Credible
Compilation with Pointers
M. Rinard, D. Marinov (MIT) |
|
|
|
| 11:00 - 11:30 |
|
Integrating
Observation Equivalence Checking and Automated Theorem Proving for Verification of Designs
at Register Transfer Level
N. Mansouri, R. Vemuri (University of Cincinnati) |
|
|
|
| 11:30 -12:00 |
|
Construction
of Verified Software Systems with Program-Checking: An Application To Compiler Back-Ends
T. Gaul, W. Zimmermann (University of Karlsruhe)
W. Goerigk (University of Kiel) |
|
|
|
| 12:00 - 12:30 |
|
Generating
Proofs from a Decision Procedure
A. Stump, D. Dill (Stanford University) |
|
|
|
| 12:30 - 14:00 |
|
LUNCH |
|
|
|
| 14:00 - 14:30 |
|
Runtime
Verification of Remotely Executed Code using Probabilistically Checkable Proof Systems
T. Batu, R. Rubinfeld, P. White (Cornell) |
|
|
|
| 14:30 - 15:00 |
|
A Type
System for Expressive Security Policies
D. Walker (Cornell) |
|
|
|
| 15:00 - 15:30 |
|
A
Formalization of the Proof-Carrying Code Architecture in a Linear Logical Framework
M. Plesko, F. Pfenning (CMU) |
|
|
|
| 15:30 - 16:00 |
|
COFFEE BREAK |
|
|
|
| 16:00 - 16.30 |
|
Value
Name Based Run-Time Checking of Computations
E. Lederer (University of Basel) |
|
|
|
| 16.30 - 17.00 |
|
Fail-Stop
Components by Pattern-Matching
T. Janowski, W. Mostowski (United Nations University) |
|
|
|
| 17.00 - 17.30 |
|
Run-Time
Result Formal Verification of Safety Critical Software: an Industrial Case Study
A. Cimatti, F. Giunchiglia, P. Traverso, A. Villafiorita (IRST) |
|
|
|
| 17.30 - 18.00 |
|
Mechanized
Result Verification: an Industrial Application
P. Bertoli, P. Traverso (IRST) |
