FME 2002 tutorial
July 20th, 2002

PVS, ICS and SAL: An introduction to the state of the art in mechanized formal methods

PVS is a mature and widely-used system for formal verification that was introduced to the world with a tutorial at FME 1993 in Odense,

For FME 2002, we offer a full-day tutorial on modern formal methods, structured in two halves. The morning will present an overview of PVS suitable for novices, followed by a description and demonstration of new capabilities that will be of interest to current users. The afternoon will introduce two new systems that complement PVS. ICS is a standalone implementation of the decision procedures from PVS that can be used to add powerful automated deductive capabilities to other software. SAL is an environment for analysis of systems specified as state machines; it serves as a tool bus that integrates existing tools such as PVS and off-the-shelf model checkers and static analyzers, and it also provides a scriptable interface that can be used to provide customized tools for abstraction and state exploration.

The tutorials will combine lectures with demonstrations of the actual systems and will focus on their use rather than underlying theory. The intended audience includes those considering using mechanized formal methods for the first time, as well as existing users of PVS and other tools.

In addition to those who will use ICS and SAL directly, the afternoon sessions are also intended for tool developers who will learn how to integrate these systems with their own. Much of the material presented should also interest those attending other FLOC conferences besides FME. Participants in the tutorial will gain insight into the different purposes and markets served by PVS, ICS, and SAL, an appreciation of their capabilities, and the basic knowledge required to start using them.

Tutorial web page

Find more about this tutorial at