2004 PROGRAM AGENDA
|
|
|
|
|
|---|---|---|---|
| 0830 - 0915 |
John Launchbury (Galois) |
Flexible Formal Methods for High Assurance: The Maude Experience |
Transparency: An Application Context for High Confidence Software and Systems (HCSS) Tools and Methods |
| 0915 - 0930 |
High Confidence Software and Systems: A Rockwell Collins Perspective |
||
| 0930 - 1000 |
Modelling Key Distribution, Art to Science |
||
| 1000 - 1015 |
|
BREAK | |
| 1015 - 1030 |
BREAK |
||
| 1030 - 1115 |
Mark P. Jones (Oregon Health and Science University) |
Theorem Provers: as High Assurance Programming Environments |
John Launchbury (Galois) |
| 1115 - 1200 |
Usage of Intermediate Java Byte Code to Verify Wireless Java Applications |
David Cooper (Praxis Critical Systems Limited) |
|
| 1200 - 1330 |
|
(Tool Demonstrations)
|
(Tool Demonstrations) |
| 1330 - 1415 |
Sir Tony Hoare (Oxford University / Microsoft Research Cambridge) |
Formally Verified Encryption of High-Level Datatypes: An Application of Polytypism |
Alessandro Coglio (Kestrel Institute) |
| 1415 - 1430 |
Ad Hoc Data: An Opportunity for Domain-specific Languages |
Anupam Datta (Stanford University) |
|
| 1430 - 1500 |
Paul Karger (IBM)
|
||
| 1500 - 1515 |
|
|
|
| 1515 - 1530 |
|
||
| 1530 - 1615 |
Joshua Guttman (The MITRE Corporation) |
Sir Tony Hoare, Helen Gill, Cordell Green, Jon Pincus, Bill Scherlis, Dickie George |
Designing and Testing a High Assurance ASN.1 Compiler |
| 1615 - 1700 |
Static Driver Verifier: Finding Device Driver Bugs at Compile-time |
(General Dynamics) |
|
| 1700 - 1715 |
Adjourn for the Day
|
Adjourn for the Day |
Conference Adjourned |
| 1715 |
Tours of the Ship |