NASA
National
November 27-30, 2007
Instructors:
Rick Butler (NASA)
Ben Di Vito (NASA)
Jeff Maddalon (NASA)
Paul Miner (NASA)
Cesar Munoz (NIA)
Radu Siminiceanu (NIA)
Day 1 Tuesday
November 27
830- 900 Check-in
60
900-1000
Introduction to Formal Modeling (
45 1000-1045 PVS Types and
Declarations (DiVito)
1045-1100 Break
60
1100-1200
Exercise 1 (
1200- 100 Lunch
45 100-
145 Expression
Language Features (DiVito)
60 145-
245 Exercise 2
(DiVito)
245- 300 Break
45 300-
345 Propositional
Logic Proving (DiVito)
45 345-
430 Exercise 3
(DiVito)
Day 2 Wednesday
November 28
45 830-
915 First/Higher
Order Proving (Miner)
60
915-1015
Exercise 4 (Miner)
1015-1030 Break
45
1030-1115
Real Number Proving (Munoz)
45
1115-1200
Strategies for Numeric Domains (Munoz)
1200- 100 Lunch
60 100-
200 Exercise 5
(Munoz)
45 200-
245 Prelude,
Libraries, Conventions (
245- 300 Break
45 300-
345 Recursion and
Induction (Miner)
60 345-
445 Exercise 6
(Miner)
Day 3 Thursday
November 29
45 830-
915 Abstract Datatypes
(Miner)
45
915-1000
Advanced Type Features (Maddalon)
1000-1015 Break
60
1015-1115
Collection Types (Maddalon)
45
1115-1200
Exercise 7 (Maddalon)
30
1200-1230
Theory Interpretations (Munoz)
1230-
130 Lunch
30 130-
200 SAL
Specification Language (Siminiceanu)
60 200-
300 SAL Model
Checking (Siminiceanu)
300- 315 Break
45 315-
400 SAL Suite:
Simulator, Advanced Tools (Siminiceanu)
45 400-
445 Exercise 8
(Siminiceanu)
Day 4 Friday
November 30
30 830-
900 Writing
Prover Strategies (Munoz)
30 900-
930 Rapid
Prototyping Using PVSio (Munoz)
30
930-1000
Proof Scripting Using ProofLite (Munoz)
1000-1015 Break
45
1015-1100
Fault Tolerance Formalisms (Miner)
30
1100-1130
Hypatheon Database of PVS Theories (DiVito)
30
1130-1200
PVS Survival Tips (
15
1200-1215
Discussion, wrap-up (