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
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.
is a standalone implementation of the decision procedures from PVS
that can be used to add powerful automated deductive capabilities to
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
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