Skip past navigation NASA Langley Formal Methods



quick page






  home > home > research

NASA LaRC PVS Class May 24-27, 2005

The Formal Methods teams at the NASA Langley Research Center and the National Institute of Aerospace 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 travel and lodging. 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 equipped to run PVS. PVS runs on Linux and Solaris as well as Mac OS X (in beta form). There is no Windows version of PVS.

We have now finalized the class content (outline appended below). Over three and a half days, we will introduce specification writing and interactive theorem proving, while interspersing a few case studies. 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 fill it the following web form .

The May 2005 course outline should give you some indication what this course will cover.


  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 26 September 2003 (10:10:40)