Class Dates: October 9 (Tuesday) - 12 (Friday)
Class Location: National Institute of Aerospace, Hampton, VA
DAY 1 • Tuesday • October 9 | ||||
Time | Lecture | Instructor | ||
---|---|---|---|---|
8:30 | 8:50 | Meet and Greet | ||
8:50 | 9:00 | Opening Remarks | ||
9:00 | 9:45 | 45 min | Introduction to Formal Methods () | Rick Butler |
9:45 | 10:15 | 30 min | PVS in a Hurry | Anthony Narkawicz |
10:15 | 10:20 | Break | ||
10:20 | 11:05 | 45 min | Exercise Set 1 | |
11:05 | 11:50 | 45 min | Types and Declarations () | Ben Di Vito |
11:50 | 1:20 | Lunch | ||
1:20 | 2:05 | 45 min | Expression Language () | Ben Di Vito |
2:05 | 2:10 | Break | ||
2:10 | 3:10 | 60 min | Exercise Set
2:chronos.pvs
|
|
3:10 | 3:55 | 45 min | Propositional Logic Proving () | Ben Di Vito |
3:55 | 4:00 | Break | ||
4:00 | 5:00 | 60 min | Exercise Set 3:prop_basic.pvs landing_weather.pvs FLT_lite.pvs FLT_lite_prop.pvs
|
DAY 2 • Wednesday • October 10 | ||||
Time | Lecture | Instructor | ||
---|---|---|---|---|
8:30 | 9:15 | 45 min | Predicate Logic Proving () | Anthony Narkawicz |
9:15 | 9:25 | Break | ||
9:25 | 10:25 | 60 min | Exercise Set 4:pred_basic.pvs FLT_lite.pvs FLT_lite_pred.pvs caucus.pvs
|
|
10:25 | 11:10 | 45 min | Prelude and NASA Libraries () | Rick Butler |
11:10 | 11:20 | Break | ||
11:20 | 11:50 | 30 min | Library Search Capability () | Ben Di Vito |
11:50 | 1:20 | Lunch | ||
1:20 | 2:05 | 45 min | Real Number Proving () | César Muñoz |
2:05 | 2:10 | Break | ||
2:10 | 3:10 | 60 min | Exercise Set 5:realproving.pvs
|
|
3:10 | 3:55 | 45 min | Collection Types () | Jeff Maddalon |
3:55 | 4:40 | 45 min | Advanced Type Features () | Jeff Maddalon |
4:40 | 4:45 | Break | ||
4:45 | 5:00 | 15 min | Exercise Set 6 (Part I) |
DAY 3 • Thursday • October 11 | ||||
Time | Lecture | Instructor | ||
---|---|---|---|---|
8:30 | 9:15 | 45 min | Exercise Set 6 (Part II) | |
9:15 | 10:00 | 45 min | Induction, Recursion, and Iteration () | César Muñoz |
10:00 | 10:05 | Break | ||
10:05 | 11:05 | 60 min | Exercise Set 7:induction.pvs
|
|
11:05 | 11:50 | 45 min | Abstract Datatypes () | Alwyn Goodloe |
11:50 | 1:20 | Lunch | ||
1:20 | 1:50 | 30 min | Exercise Set 8:abstract_datatypes.pvs
|
|
1:50 | 2:35 | 45 min | Theory Interpretations () | Sam Owre |
2:35 | 3:05 | 30 min | Animation of Functional Specifications () | César Muñoz |
3:05 | 3:10 | Break | ||
3:10 | 3:40 | 30 min | Computational Reflection () | Anthony Narkawicz |
3:40 | 4:10 | 30 min | Proof Scripting and Strategy Writing () | César Muñoz |
4:10 | 4:15 | Break | ||
4:15 | 5:00 | 45 min | Exercise Set 9:strat.pvs pvs-strategies
|
DAY 4 • Friday • October 12 | ||||
Time | Lecture | Instructor | ||
---|---|---|---|---|
8:30 | 9:30 | 60 min | Invited Talk: PVS 6.0 and Beyond () | Sam Owre |
9:30 | 9:40 | Break | ||
9:40 | 10:10 | 30 min | Nonlinear Arithmetic Proving () | Anthony Narkawicz |
10:10 | 10:55 | 45 min | Linear Algebra () | Heber Herencia |
10:55 | 11:05 | Break | ||
11:05 | 11:50 | 45 min | Survival Tips and Conclusion () | Rick Butler |
11:50 | 12:00 | Closing Remarks |