[PVS] PVS Training Class -- NASA/NIA -- November 27-3, 2007

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 in Winter 2007 on SRI International's PVS Specification and Verification System (http://pvs.csl.sri.com). The class will take place November 27-30, 2007 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.

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.

The class announcement is available at

http://shemesh.larc.nasa.gov/fm/PVS-Class-2007-Announcement.html

If you would like to register for the course visit

http://shemesh.larc.nasa.gov/fm/fm-PVS-class-reg.html

This announcement may be freely distributed.

Ricky W. Butler

1 South Wright Street, MS 130

NASA Langley Research Center

Hampton, VA 23681 USA

757-864-6198