Overview

This is a one-day workshop on Integrated Formal Methods based around the SRI tools PVS, ICS, and SAL. The workshop will include a half-day tutorial on the novel and advanced features of these systems, and another half-day session devoted to contributed talks detailing practical experience with the use and integration of these tools.

Program

• AFM program

Invited Talk

• Monday, August 21st, 14:00‑15:00
  Joseph Kiniry (School of Computer Science and Informatics, University College Dublin, Dublin, Ireland)
  (Deeply) Integrating Programming and Proving [pdf]

Tutorials

• Monday, August 21st, 09:00‑09:30
  John Rushby (SRI)
  Overview of PVS, ICS, and SAL, and plans for the future [pdf]
• Monday, August 21st, 09:30‑10:00
  Sam Owre (SRI)
  Recent PVS Language Developments [pdf]
• Monday, August 21st, 10:00‑10:30
  N. Shankar (SRI)
  Recent PVS Prover Developments [pdf]
• Monday, August 21st, 11:00‑11:30
  Leonardo de Moura (SRI)
  Overview of ICS/Yices [pdf]
• Monday, August 21st, 11:30‑12:00
  John Rushby (SRI)
  Overview of SAL: Model Checking and Test Generation [pdf]
• Monday, August 21st, 12:00‑12:30
  Bruno Dutertre (SRI)
  Model Checking Infinite-state Systems in SAL [pdf]

Further Details

PVS (Prototype Verification System) is an established general-purpose verification system built around an expressive specification language and an interactive theorem prover that integrates a variety of powerful inference procedures include ground decision procedures, rewriting, the MONA procedure for monadic second-order logic, and symbolic model checking. 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 tutorial session 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, tool developers who will learn how to integrate these systems with their own. Much of the material presented should also interest those attending the FLOC conferences. 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.

The contributed session will include talks from within the user community of PVS, ICS, and SAL. These contributions will report on experiments carried out with these tools, experience integrating these tools into other systems, and comparisons with other comparable tools. Lecture materials, together with the systems, will be available from SRI's web site prior to the tutorial.

The presenters will include John Rushby and N. Shankar. Successful tutorials on PVS were held at FME 93, 96, and 99 (the latter two each attracting over 100 participants).

PVS, ICS, and SAL are available under license from SRI; there is no charge for research and educational use.