[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

PVS Class April 22-25, 2003 in Hampton, Va.



Dear Colleague,

We will be offering a PVS Class April 22-25, 2003 in Hampton, Va.  The 
course will be offered free of charge and will be held off-site so that 
non-US citizens can attend.   We only have a limited number of laptops 
available, so it will be necessary for you to bring a laptop to get full 
benefit from the course. Otherwise you will probably have to pair up with 
someone else who brought one. If you would like to attend, please fill out 
the attached registration form. If you have any questions don't hesitate to 
send them to me (r.w.butler@larc.nasa.gov) or Ben Di Vito at 
(b.l.divito@larc.nasa.gov.)

We offer these free courses as a public service to the technical 
community.  In return, we expect the attendees to bear the burden and cost 
of traveling to our site.

Please feel free to pass this announcement along to others.

Rick Butler

P.S.   Ben Di Vito will be in charge of the course content and I will be 
handling the administrative matters.


See attachments for details.

Rick Butler
Day 1  Tuesday 

          830- 900     Check-in
          900-1000     Introduction to Formal Modeling (Butler)
         1000-1045     PVS Types (DiVito)
         1045-1100     Break
         1100-1200     Exercise 1 (Butler)
         1200- 100     Lunch
          100- 145     Basic PVS Language (DiVito)
          145- 245     Exercise 2 (DiVito)
          245- 300     Break
          300- 315     PVS Proof Theory (Miner)
          315- 345     Propositional Logic Proving (DiVito)
          345- 430     Exercise 3 (DiVito)

Day 2  Wednesday 

          830- 900     First Order Proving (DiVito)
          900-1000     Exercise 4 (DiVito)
         1000-1015     Break
         1015-1100     Recursion and Induction (Miner)
         1100-1200     Exercise 5 (Miner)
         1200- 100     Lunch
          100- 145     Advanced Type Features (Gottliebsen)
          145- 245     Collection Types (Butler)
          245- 300     Break
          300- 330     Prelude, Libraries (Gottliebsen)
          330- 430     Exercise 6 (Butler/Gottliebsen)

Day 3  Thursday 

          830- 915     Abstract Datatypes (Miner)
          915-1000     State Machine Modeling (DiVito)
         1000-1015     Break
         1015-1100     State Machine Proving (Butler)
         1100-1200     Exercise 7 (Butler)
         1200- 100     Lunch
          100- 145     Rewrite Rules (Geser)
          145- 230     Real Number Proving (Munoz)
          230- 245     Break
          245- 345     Prover Strategies (Munoz)
          345- 430     Exercise 8 (Munoz/Geser)

Day 4  Friday

          830- 900     Tabular Specifications (DiVito)
          900- 930     Proof Automation Case Study (DiVito)
          930-1030     Exercise 9 (DiVito)
         1030-1045     Break
         1045-1130     PVS Survival Tips (Butler)
         1130-1200     Additional Topics, Discussion (Butler)


			        REGISTRATION FORM
	  NASA Langley Training Course in PVS Theorem Prover

We will be offering a 3 1/2 day PVS Class April 22-25, 2003 at the new National Institute for Aerospace located in Hampton, Virginia near the Langley Research Center. The course is free of charge and open to both US citizens and non-US citizens.  We only have a limited number of laptops available, so it will be necessary for you to bring a laptop with Linux installed to get full benefit from the course. Otherwise you will probably have to pair up with someone else who brought one.

NAME:          _______________________________________
ADDRESS:       _______________________________________ 
               _______________________________________ 
               _______________________________________ 
               _______________________________________ 
PHONE NUMBER:  _______________________________________
EMAIL ADDRESS: _______________________________________

Please answer the following questions:
(1) I am able to bring a laptop
    a. No
    b. Yes
    c. and I can install Linux on it before I come
    d. and I can install Linux and PVS 3.0 on it before I come
(2) Knowledge of Emacs
    a. I know nothing
    b. minimal
    c. experienced
    d. expert
(3) Knowledge of Mathematical Logic
    a. I know nothing
    b. minimal
    c. one semester course
    d. extensive knowledge
(4) Experience with PVS
    a. I know nothing
    b. Can read PVS specs
    c. Have done some proofs
    d. I just need the advanced stuff


Email registration form to R.W.Butler@larc.nasa.gov or send by postal mail to

  Ricky W. Butler
  Mail Stop 130
  1 South Wright Street
  Building 1220, Room 126A
  NASA Langley Research Center
  Hampton, VA 23681-2199

We will send directions and hotel info to those who register. If you have any questions don't hesitate to send them to me (r.w.butler@larc.nasa.gov) or Ben Di Vito at(b.l.divito@larc.nasa.gov.)
Dear Colleague,

We will be offering a PVS Class April 22-25, 2003 in Hampton, Va.  The course will be offered free of charge and will be held off-site so that non-US citizens can attend.   We only have a limited number of laptops available, so it will be necessary for you to bring a laptop to get full benefit from the course. Otherwise you will probably have to pair up with someone else who brought one. If you would like to attend, please fill out the attached registration form. If you have any questions don't hesitate to send them to me (r.w.butler@larc.nasa.gov) or Ben Di Vito at (b.l.divito@larc.nasa.gov.) 

We offer these free courses as a public service to the technical community.  In return, we expect the attendees to bear the burden and cost of traveling to our site.  

Please feel free to pass this announcement along to others.

Rick Butler

P.S.   Ben Di Vito will be in charge of the course content and I will be handling the administrative matters.