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.
