Skip past navigation NASA Langley Formal Methods



quick page






  home > research

PVS Class 2007 Announcement

The Formal Methods teams at NASA Langley Research Center and the National Institute of Aerospace are offering a short course in Winter 2007 on SRI International's PVS Specification and Verification System. The class will take place November 27-30 at National Institute of Aerospace, 100 Exploration Way Room 101, Hampton, VA 23666. 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. For more information about the course content, see class description. A tentative agenda is available at

This class will include some new material including a brief introduction to the SAL model checker and the YICES SMT Solver, which were also developed by SRI International. The length of these new sessions will be determined by participant interest.

If you would like to register for the course go to:

PVS Class 2007 Registration


  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: 10 December 2002 (10:59:47)