**Course Description - NASA Langley/NIA Short Course on Formal Methods
Using PVS**

**Designed for**

The target audience for this course includes systems engineers and
architects, designers and developers of software and digital hardware
components, technical personnel involved in the verification and
validation of critical software subsystems, certification authorities
for critical systems, and researchers concerned with dependable
computing technology.

**Goal**

This 3.5 day course introduces a deductive approach to rigorous
verification for critical systems. It is based on the application of
formal logic, mathematical models and interactive theorem proving. SRI
International\'s PVS Specification and Verification System is the
particular tool we use and teach.

**Learning Outcome(s)**

Through this course you will appreciate the role played by formal
methods in the verification and analysis of dependable computing
systems. You will acquire an understanding of logical concepts and see
them applied to the analysis of software designs and algorithms. You
will have an opportunity to try a particular mechanization of these
methods (PVS) and be well positioned to learn about other methods after
completing the course.

**Learning Methods**

The Formal Methods teams at NASA Langley Research Center and the
National Institute of Aerospace offer this short course on mechanized
formal methods. Presented on a semi-regular basis, the course emphasizes
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 and work through the exercises.
Over three and a half days, we introduce specification writing and
interactive theorem proving, while interspersing a few case studies.

We have conducted this course several times in the past, most recently
in May 2005. Our policy has been to offer the course free of charge as a
public service to the technical community. In return, attendees bear the
cost of traveling to the course venue, which is typically NIA's
near-site educational facilities in Hampton, Virginia.

**Specific Objectives**

Upon completion of this course, you will be able to:

-   Apply concepts of logical deduction and inference to the software
    development and verification process.

-   Express simple models, requirements and designs in the PVS formal
    specification language.

-   Make use of the PVS interactive theorem prover to construct
    rigorous, deductive proofs of software properties or pure
    mathematical results.

-   Apply the logic-based modeling and analysis methods to small case
    studies of software component designs.

    **Key Topics**

-   Introduction to formal modeling

-   The PVS verification environment

-   Expressing formal specifications in PVS

-   Basic interactive theorem proving

-   Using recursion and induction

-   Collections and advanced type features

-   State machine modeling and proving

-   Libraries and strategies

-   Real number proving

-   Emerging capabilities

    **Prerequisites**

Understanding of basic principles of software design and implementation,
knowledge of elementary undergraduate mathematics, a passing familiarity
with concepts of logic and mathematical proof, and the ability to carry
out modest tasks on a Unix-family workstation.

# 

**References:**

-   <http://shemesh.larc.nasa.gov/fm/>

-   <http://research.nianet.org/fm-at-nia/>

-   [http://pvs.csl.sri.com](http://pvs.csl.sri.com/)/

    **Course Instructors:**

    Ricky Butler

Ben Di Vito

Jeff Maddalon

Paul Miner

Cesar Munoz (NIA)

Radu Siminiceanu (NIA)

**NASA Point of Contact:**

Ricky W. Butler\
1 South Wright Street, MS 130\
NASA Langley Research Center\
Hampton, VA 23681\
757-864-6198