NASA/NIA PVS Class 2012 • Program

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