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

[PVS] NASA Langley - NIA training course on PVS

Dear Colleague,

The Formal Methods teams at NASA Langley Research Center 
(http://shemesh.larc.nasa.gov/fm) and the National Institute of Aerospace 
(http://research.nianet.org/fm-at-nia) are offering a short course on PVS in 
the spring of 2005.  The class will take place May 24-27 in Hampton, 
Virginia.  We have conducted this course several times in the past, most 
recently in April 2003.  Our policy is to offer the course free of charge as 
a public service to the technical community.  In return, attendees bear the 
cost of traveling to our site.  The class is open to all interested 
individuals, including non-US citizens.

We emphasize a hands-on, immersion-style learning approach.  Both lecture 
material and in-class exercises using PVS are featured.  For this reason, we 
strongly encourage attendees to bring a laptop.  Over three and a half days, 
we introduce specification writing and interactive theorem proving, while 
interspersing a few case studies.

Although we have not yet finalized the class content, it will be similar to 
what we offered in 2003 (see attached outline).  Included on the agenda will 
be a presentation and demo of the Zeus/PVS toolset. Developed by Prof. John 
Knight and his group at the University of Virginia, Zeus/PVS is a 
comprehensive framework for creating and analyzing formal specifications.

If you would like to register for the course or learn more about it, contact 
the coordinator:

Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883
fax: +1-757-864-4234

Alternatively, you may reach Rick Butler (r.w.butler@larc.nasa.gov, 
757-864-6198), who leads the formal methods team at NASA Langley.

Please send full contact information with your registration request. In 
addition, to help us fine tune the class arrangements, we would appreciate 
your providing us with the following information:

 - Whether you can bring a laptop with Linux installed.  (PVS runs
   on a limited set of platforms.  A Linux-equipped laptop is the
   best option.  We can provide a few loaners.)

 - Whether you are experienced with Emacs or have a minimal comfort
   level with the Emacs editor.

 - What level of familiarity you have with mathematical logic.

 - What degree of prior knowledge or experience you have with PVS.

We are open to any additional thoughts about how this course might be 
structured.  If there is sufficient interest, we can tailor the schedule to 
include specialized topics.  Send us your ideas and we will consider them.

Best regards,

Ben Di Vito

P.S.  Please forward this announcement to others who might have an interest in 

	    NASA Langley PVS Training Class

            National Institute of Aerospace
            144 Research Drive
	    Hampton, Virginia 23666

		April 22-25, 2003

Day 1  Tuesday April 22

          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 April 23

          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 April 24

          830- 915     Rewrite Rules (Geser)
          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- 400     Prover Strategies (Munoz)
          400- 445     Exercise 9 (Munoz)

Day 4  Friday April 25

          830- 900     Tabular Specifications (DiVito)
          900- 945     Abstract Datatypes (Miner)
          945-1015     PVS Survival Tips (Butler)
         1015-1030     Break
         1030-1130     Emerging Capabilities
                         Zeus/PVS Toolset (Univ. of Virginia)
                         Ground Evaluator and PVSio (Munoz)
                         Formal Specifications Database (DiVito)
         1130-1145     Discussion, wrap-up (Butler)

  Optional, for those interested:

         1145-????     Demo of Zeus/PVS (Univ. of Virginia)