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 |