NASA Langley - NIA Short Course on PVS
ODU Peninsula Graduate Center
Room 2262
600 Butler Farm Road
Hampton, Virginia 23666
May 24-27, 2005
Instructors:
Rick Butler (NASA)
Ben Di Vito (NASA)
Jeff Maddalon (NASA)
Paul Miner (NASA)
Cesar Munoz (NIA)
Lee Pike (NASA)
Day 1 Tuesday May 24
830- 900 Check-in
900-1000 Introduction to Formal Modeling (Butler)
1000-1045 PVS Types and Declarations (DiVito)
1045-1100 Break
1100-1200 Exercise 1 (Butler)
1200- 100 Lunch
100- 145 Expression Language Features (DiVito)
145- 245 Exercise 2 (DiVito)
245- 300 Break
300- 345 Propositional Logic Proving (Pike)
345- 430 Exercise 3 (Pike)
Day 2 Wednesday May 25
830- 915 First/Higher Order Proving (Pike)
915-1015 Exercise 4 (Pike)
1015-1030 Break
1030-1115 Recursion and Induction (Miner)
1115-1215 Exercise 5 (Miner)
1215- 115 Lunch
115- 200 Abstract Datatypes (Miner)
200- 245 Advanced Type Features (Maddalon)
245- 300 Break
300- 400 Collection Types (Maddalon)
400- 445 Exercise 6 (Maddalon)
Day 3 Thursday May 26
830- 915 Prelude, Libraries, Conventions (Butler)
915-1000 State Machine Modeling (DiVito)
1000-1015 Break
1015-1100 State Machine Proving (Butler)
1100-1200 Exercise 7 (Butler)
1200- 100 Lunch
100- 200 Real Number Proving (Munoz)
200- 245 Exercise 8 (Munoz)
245- 300 Break
300- 345 Prover Strategies (Munoz)
345- 445 Emerging Capabilities I
Univ. of Virginia's Zeus/PVS Toolset
(John Knight, Sean Travis)
445- ??? Optional: Q&A, hands-on demo with Zeus/PVS
Day 4 Friday May 27
830- 900 Theory Interpretations (Munoz)
900- 945 Fault Tolerance Formalisms (Miner)
945-1015 PVS Survival Tips (Butler)
1015-1030 Break
1030-1200 Emerging Capabilities II
Rapid Prototyping Using PVSio (Munoz)
Hypatheon Database of PVS Theories (DiVito)
SAL: SRI's Symbolic Analysis Lab (Pike)
1200-1215 Discussion, wrap-up (Butler)