2007 PROGRAM AGENDA
|
TUESDAY, MAY 8 |
WEDNESDAY, MAY 9 |
THURSDAY, MAY 10 | ||
| 0830 - 0845 | Trusted Services Engine (TSE) and Applications Andy Adams-Moran (Galois) |
Welcome and Introductions |
Compositional Assurance for MILS |
|
|
Formal Specifications on Industrial Strength Code: From Myth to Reality |
||||
| 0845 - 0915 | ||||
| 0915 - 0945 |
Pete Manolios |
|||
| 0945 - 1000 |
BREAK |
|||
| 1000 - 1030 | BREAK |
Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution |
Verifying an Operating System Kernel |
|
| 1030 - 1045 |
Andy-Adams Moran |
|||
| 1045 - 1100 |
Static Analysis for |
BREAK |
||
| 1100 - 1130 |
Formally Verified ARM Code |
|||
| 1130 - 1145 | Formal Methods Anecdotes: Worse is Better! Dan Craigen (CSE) |
|||
| 1145 - 1200 |
Circuit Specification, Abstraction, |
|||
| 1200 - 1215 |
LUNCH |
|||
| 1215 - 1230 | LUNCH | |||
| 1230 - 1330 | LUNCH | |||
| 1330 - 1345 |
Byron Cook |
|||
| 1345 - 1400 |
Trust Relationships |
A Formal Semantics for ASN.1 |
||
| 1400 - 1430 | ||||
| 1430 - 1445 |
Manifest Safety and Security |
|||
| 1445 - 1500 |
BREAK |
|||
| 1500 - 1515 | BREAK |
Turnstile: A High-Assurance |
||
| 1515 - 1530 |
BREAK |
|||
| 1530 - 1600 |
Byron Cook |
Justifiable Confidence? |
||
| 1600 - 1615 |
The Haskell Lightweight VM |
|||
| 1615 - 1700 |
The Verified Software Initiative |
|||
| 1700 |
Adjourn for the Day |
Adjourn for the Day |
Conference Adjourned |
|
| 1830 |
Conference Dinner |
|||
