Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

PVS Old User Links

This page provides links to descriptions of various pieces of work undertaken by users of PVS. The list is a little out of date, and we encourage you to update your entry and submit new entries. If you would like your work linked, please fill in this form, or send email to Rushby@csl.sri.com. (Please read these suggestions about publishing on the Web first!)

If you have problems downloading papers, check this troubleshooting page.

There is also a list of PhD Theses by PVS Users.

Fast links: Bordeaux | Bremen | Collins | Cottbus | de Montfort | Dresden | Eindhoven | Fujitsu | GEC | Indiana | JPL | Kiel | London | LSI Logic | Manchester | Milano | Minnesota | Namur | Nijmegen | NASA Langley | NRL | Paris VI | Philips | Princeton | Southampton | SCC | SRI | Stanford | Tampere | Ulm | Utah | Utrecht | Verimag | Virginia | Weizmann | York

University of Bordeaux

Imperative Program Verification

Paul Gloess of the University of Bordeaux has made his PVS libraries for permutations and well-founded relations available, together with the proof of a simple compiler (which illustrates the ground evaluator). The link above also provides access to his PVS formalization of the language L2 from the book "The foundations of Program Verification" by Loeckx and Sieber, together with a collection of PVS theories and strategies that assist in the mechanical proof of total correctness of imperative programs.

University of Bremen

Combination of PAMELA and PVS

Bettina Buth has developed an interface between her PAMELA system for verifying VDM-style specifications and PVS. A draft report is available, and the tool will be demonstrated at AMAST in Australia.

Collins Commercial Avionics

Microprocessor Verification

Collins Commercial Avionics and SRI have been undertaking the formal specification and verification of a commercial avionics processor called the AAMP5, which is a faster version of the AAMP2 (there are 30 AAMP2s on board each Boeing 747-400). The AAMP5 is both pipelined and microcoded; there are approximately 500,000 transistors in its implementation. A paper describing this project is available entitled Formal Verification of the AAMP5 Microprocessor--A Case Study in the Industrial Use of Formal Methods by Steven P. Miller of Collins Commercial Avionics and M. Srivas of SRI. For more technical detail, see their paper from CHDL '95, and for full details see their technical report

Current work is aimed at complete formal verification of a simpler processor of the kind used for truly critical avionics applications.

Cottbus University

The Invoicing Example

Heinrich Rust has undertaken a PVS version of the Invoicing'98 example

de Montfort University

A Compositional Approach to the Specification of Systems using ITL and Tempura

Antonio Cau and colleagues are using PVS for checking Interval Temporal Logic (ITL) proofs, and have made a PVS ITL library available.

Technical University of Dresden

Coalgebraic Datatypes

Ulrich Hensel (with Bart Jacobs of Nijmegen) has been using PVS in formalizing coalgebraic datatypes (such as sequences) and their proof principles.

Technical University of Eindhoven

Real Time

Jozef Hooman at the Technical University of Eindhoven in the Netherlands, has used PVS to provide mechanical support for the Correctness of Real-Time Systems by Construction

He presented a paper Verifying Part of the ACCESS.bus Protocol Using PVS at the 15th Conference on the Foundations of Software Technology and Theoretical Computer Science held in Bangalore, India, in December 1995.

Jozef and Jan Vitt also have a paper on an Assertional Specification and Verification Using PVS of the Steam Boiler Control System, which was presented at the recent Dagstuhl Workshop on Reactive Systems

Jozef has also recently completed the final version of a paper describing use of PVS to specify and verify the RPC-Memory Specification Problem proposed by Manfred Broy and Leslie Lamport for another Dagstuhl seminar held in September '94.

Fujitsu Laboratories of America

ATM Switches

Researchers at Fujitsu have used PVS in conjunction with other tools to verify the design of an ATM switch.

A paper High-Level Design and Validation of ATM Switch by S.P. Rajan, M. Fujita, K. Yuan, and M. T-C. Lee was presented at the IEEE International High Level Design Validation and Test Workshop, Nov. 1997, pp. 40--44.

Another wil be presented at AMAST: Conference on Algebraic Methodology and Software Technology 13-17 December 1997, Sydney Australia.

GEC Marconi Avionics

SafeFM

Researchers at GEC Marconi Avionics and AEA Technology are using PVS in the SafeFM project in collaboration with London University.

GEC are a bit reticent about putting their reports on the web. You can request them from Bowen.Ormsby@gecm.com.

Indiana University

Derivation of Digital Circuits

Paul S. Miner, Shyamsundar Pullela, and Steven D. Johnson of Indiana University developed a circuit for clock synchronization using a combination of DDD, PVS, and a BDD package: Interaction of Formal Design Systems in the Development of a Fault-Tolerant Clock Synchronization Circuit, presented at the 13th Symposium on Reliable Distributed Systems, October 1994, Dana Point, CA, pp. 128--137. Here's the technical report version (postscript only)

Further developments are described in Verification of an optimized fault-tolerant clock synchronization circuit: A case study exploring the boundary between formal reasoning systems by Paul S. Miner and Steven D. Johnson, presented at the conference on Designing Correct Circuits in Bastad, Sweden in September 1996.

Comparative Study (Joint with NASA Langley)

Steven D. Johnson, Paul S. Miner, and Albert Camilleri of Indiana University, NASA Langley, and HP, did a study of the "Single Pulser" circuit for TPCD using various reasoning tools, including PVS (and SMV, DDD, and Oct Tools). Studies of the Single Pulser in Various Reasoning Systems (postscript only). See the ftp directory at Indiana for additional information.

Kathi Fisler of Indiana, in another paper presented at TPCD, describes how diagrams can be used to represent hardware proofs using the PVS proof from the previous paper as an example: Extending Formal Reasoning with Support for Hardware Diagrams (postscript only)

Jet Propulsion Laboratory

Cassini Spacecraft

Yoko Ampo of NEC Space Systems and Robyn Lutz of JPL and Iowa State University at Ames have applied formal methods using PVS to aspects of the Cassini spacecraft (a Saturn orbiter due for launch in 1997).

JPL has rather restrictive policies for putting their material on the Web, but copies of these papers are available from the authors, or from us.

Requirements Analysis (Joint with NASA Johnson Space Center)

David Hamilton (IBM/Loral/Lockheed Space Systems), Rick Covington (JPL), John Kelly (JPL), and Alice Lee (JSC) describe some NASA multi-center experiments in applying formal methods with PVS to software requirements for spacecraft (mainly the Space Shuttle).

As noted previously, JPL has rather restrictive policies about putting their material on the Web, but copies of these papers are available from the authors, or from us.

Indiana University

Derivation of Digital Circuits

Paul S. Miner, Shyamsundar Pullela, and Steven D. Johnson of Indiana University developed a circuit for clock synchronization using a combination of DDD, PVS, and a BDD package: Interaction of Formal Design Systems in the Development of a Fault-Tolerant Clock Synchronization Circuit, presented at the 13th Symposium on Reliable Distributed Systems, October 1994, Dana Point, CA, pp. 128--137. Here's the technical report version (postscript only)

Further developments are described in Verification of an optimized fault-tolerant clock synchronization circuit: A case study exploring the boundary between formal reasoning systems by Paul S. Miner and Steven D. Johnson, presented at the conference on Designing Correct Circuits in Bastad, Sweden in September 1996.

Comparative Study (Joint with NASA Langley)

Steven D. Johnson, Paul S. Miner, and Albert Camilleri of Indiana University, NASA Langley, and HP, did a study of the "Single Pulser" circuit for TPCD using various reasoning tools, including PVS (and SMV, DDD, and Oct Tools). Studies of the Single Pulser in Various Reasoning Systems (postscript only). See the ftp directory at Indiana for additional information.

Kathi Fisler of Indiana, in another paper presented at TPCD, describes how diagrams can be used to represent hardware proofs using the PVS proof from the previous paper as an example: Extending Formal Reasoning with Support for Hardware Diagrams (postscript only)

University of Kiel

Stepwise Refinement

Jens Knappmann developed a tool for developing programs by stepwise refinement using PVS, as part of his Master's Thesis.

Compiler Verification

A ProCoS project report by Karl-Heinz Buth of the University of Kiel on Automated Code Generator Verification Based On Algebraic Laws using PVS is available (from Germany; there's also a copy here in the US).

London University (Royal Holloway and Bedford New College, and Queen Mary and Westfield College) with GEC Marconi Avionics

SafeFM

Researchers at these two colleges of the University of London, led by Victoria Stavridou and in collaboration with GEC Marconi Avionics and AEA Technology, are using PVS in the SafeFM project, concerned with the practical application of formal methods to safety critical systems. A paper Formal Requirements Analysis of an Avionics Control System by Bruno Dutertre and Victoria Stavridou that appears in the May 1997 issue of IEEE Transactions on Software Engineering (Vol. 23, No. 5, pp. 267--278) provides an overview. In support of work aimed at formalizing hybrid systems, Bruno Dutertre has developed a body of classical concepts and results in mathematical analysis using PVS. He presented a paper Elements of Mathematical Analysis in PVS at TPHOLs'96, held in Turku, Finland, 27-30 August 1996. The library of PVS theories developed by Bruno is available by ftp from http://www.csl.sri.com/~bruno/pvs-stuff.html

Other papers on SafeFM, and additional applications of PVS, are available from the home page of Bruno Dutertre

LSI Logic

Protocol Specification

Vijay Nagasamy of LSI Logic, Sreeranga Rajan (then of SRI), and Preeti R. Panda of UC Irvine recently presented a paper on Fiber channel protocol: Formal specification and verification at the Sixth Annual Silicon Valley Networking Conference. They specified a portion of an implementation of the protocol in PVS and used the PVS model checker to examine its properties.

University of Manchester

Verification for ELLA

Ella is a UK hardware description language. A group at Manchester University has developed a verification environment for Ella that uses PVS as a back-end.

Politecnico di Milano

TRIO Specification Analysis

A group in the Dipartimento di Elettronica e Informazione at the Politecnico di Milano is using PVS to support mechanized analysis of TRIO specifications.

University of Minnesota and Michigan State University

Tabular Specifications in RSML

Mats Heimdahl at the University of Minnesota and Barbara Czerny at Michigan State, E. Lansing, have been using PVS to discharge proof obligations from tabular specifications expressed in RSML. They presented a paper Using PVS to Analyze Hierarchical State-Based Requirements for Completeness and Consistency at the IEEE High Assurance in Systems Engineering Workshop, Niagra Falls, Canada, in October 1996.

The disappointing results when they applied PVS to their large examples are being addressed with new prover components and organization and we expect to be able to handle these easily by early 1998. (The formulas concerned are not tautologies; the PVS BDD package discovers this in a few seconds; PVS then calls the BDD package a second time to generate a minimal set of sequents to display to the user. It was this second call that was not terminating since the minimal set contains thousands of sequents. When the BDD package is incorporated as a foreign function [as opposed to an external call, as it is at present], we will be able to exert more control and will not attempt this minimization when there are large numbers of sequents.)

Other papers by Mats on this topic include

University of Namur, Belgium

Formal RE Languages

Philippe Du Bois, Eric Dubois, and Jean-Marc Zeippen presented a paper On the Use if a Formal RE Language: The Generalized Railroad Crossing Problem at the 3rd IEEE International Symposium on Requirements Engineering, Annapolis, MD, January 1997. They describe the Albert II specification language and their plans to use PVS to provide reasoning support.

University of Nijmegen

Coalgebraic Datatypes

Bart Jacobs has been using PVS in formalizing coalgebraic datatypes (such as sequences)

NASA Langley Research Center

NASA Langley Research Center Formal Methods Program

Elementary Tutorial

Ricky Butler of NASA Langley has developed An Elementary Tutorial on Formal Specification and Verification Using PVS. It's available in postscript or as a hypertext document Note, a revised version, updated to PVS 2, and a more advanced version are also available.

Floating Point Arithmetic

In a paper presented at the HOL User's Workshop, HUG '95, Victor Carreno and Paul Miner of NASA Langley, develop some of the IEEE 854 Floating Point standard in both PVS and HOL. Full details of the PVS specification are available in a technical report

In a paper presented at FMCAD '96, Paul Miner and Jim Leathrum (of Old Dominion University), discuss Verification of IEEE Compliant Subtractive Division Algorithms. The PVS specification files are also available.

Requirements

In a paper presented at Formal Methods Europe (FME '96), Ben Di Vito of NASA Langley describes Formalizing New Navigation Requirements for NASA's Space Shuttle. A technical report by Ben Di Vito and Larry Roberts provides full details: Postscript, or Adobe Acrobat (PDF)

Rick Butler provides An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot in NASA Technical Memorandum 110255 of May 1996.

US Naval Research Laboratory

US Naval Research Laboratory

Verification of Timed Automata

Myla Archer and Connie Heitmeyer of NRL have been developing a system on top of PVS that is specialized for verifying the IO and timed automata of Nancy Lynch. The system and its applications are described in the following papers.

University of Paris VI

Protocol Verification

In joint work with Shankar of SRI, Klaus Havelund of LITP, Institut Blaise Pascal, University of Paris VI, presented a paper at Formal Methods Europe (FME '96) on Experiments in Theorem Proving and Model Checking for Protocol Verification

Philips, Eindhoven

Digital Synthesis

Sreeranga Rajan, then a student from the University of British Columbia, visited Philips Research Laboratories in the Netherlands during the winter of 1993-4, where he applied PVS to Transformations in High-Level Synthesis: Formal Specification and Efficient Mechanical Verification (see also his PhD Thesis). A paper on this work has recently appeared in ACM TODAES.

Sree was a student visitor at CSL from 1994 to 1995, where he extended PVS to use a BDD-based decision procedure for Park's mu-calculus from the Technical University of Eindhoven. This is used to provide CTL model checking in PVS.

Princeton University

Security of Java-style Dynamic Linking

Drew Dean of Princeton spent the summer of 1996 at SRI, where he used PVS to model security aspects of the dynamic linking used in Java. This work is described in The Security of Static Typing with Dynamic Linking, to be presented at the 4th ACM Computer and Communications Symposium, Zurich, Switzerland, April 1997.

Secure Computing Corporation (SCC)

Compositional Methods for Security

Researchers at SCC have used PVS to formalize a framework for the composition of secure systems from components, and have also verified example compositions. A report and some further links are available.

University of Southampton

Support for B Abstract Machine Notation

Chris Pratten has developed an AMN-PROOF Tool, which generates proof obligations for the Abstract Machine Notation (AMN) of J-R Abrial's B Method. The proof obligations are in a form suitable for consideration by HOL or PVS.

Stanford University

Cache Coherence Protocols and Memory Models

Seungjoon Park has developed a new and systematic way to generate the abstraction functions used in verification of concurrent systems and applied the method to verification of the FLASH cache coherence protocol using PVS.

We have a collaborative project with David Dill's group at Stanford to combine theorem proving and state exploration/model checking techniques.

Tampere University of Technology

Mechanized verification for DisCo

Pertti KellomŠki is using PVS to support mechanized verification for the DisCo specification method for reactive systems. Papers are available from Pertti's papers page and from the DisCo verification page.

University of Ulm

PVS @ Ulm

Program Transformations and Compilation

Axel Dold of the University of Ulm, Germany presented a paper on Representing, Verifying and Applying Software Development Steps using the PVS system at the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST '95). The paper is available in postscript from either SRI (USA) or Ulm (Germany). See also Ulm Technical Report, no. UIB-94-10 "Formalisierung schematischer Algorithmen" (in German) for a description of the formalization and verification of global search theory using PVS. Available from Ulm in postscript only.

Also available is a techical report A Generic Specification for Verifying Peephole Optimizations by A. Dold, F. W. von Henke, H. Pfeifer, and H. Rue§. It describes a case study carried out within the Verifix project on compiler verification.

The Typelab home page describes a project that is building an environment similar to PVS, but for a much richer type theory.

Harald Ruess presented a paper Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study at FMCAD, Springer-Verlag LNCS 1166, pp. 79-93, November 1996, Palo Alto CA.

University of Utah

Distributed Systems

The Utah Verifier project under the direction of Ganesh Gopalakrishnan and Alan Davis aims to address problems in making formal verification techniques apply to problems of industrial scale. Some of its components are based on PVS. Papers pertaining to pipelined processor verification and shared memory system design and I/O protocol verification, as well as slides of talks are available online.

Utrecht University

Utrecht University

Distributed Systems

Frank de Boer and Marten van Hulst of the Department of Computer Science at Utrecht University presented a paper at Formal Methods Europe (FME '96) on Local Nondeterminism in Asynchronously Communicating Processes. Marten's PhD Thesis is also available.

VERIMAG (Grenoble, France)

VERIMAG

Automated Generation of Invariants

Saddek Bensalem (VERIMAG, visiting SRI), Yassine Lakhnech (Kiel), and Hassen Saidi (VERIMAG) presented a paper at CAV '96 titled Powerful Techniques for the Automatic Generation of Invariants (LNCS 1102, pp. 323-335)

Susanne Graf, David Lesens, and Hassen Saidi have developed tools for proving invariance properties of concurrent systems that uses PVS as a back-end. The first two papers provide overviews.

University of Virginia

Security

Ramesh V. Peri, William A. Wulf, and Darrell M. Kienzle have developed A Logic of Composition for Information Flow Predicates, which they presented at the 9th IEEE Computer Security Foundations Workshop in Kenmare, Ireland, June 1996. Their framework, which is specified in PVS, allows proof of certain security composition properties to be proved automatically.

Weizmann Institute

TPVS

Three students at the Weizmann Institute, Alexander Blinchevsky, Boris Liberman, and Ilya Usvyatsky, are developing a "Temporal Prototype Verification System" (TPVS) under the supervision of Prof. Amir Pnueli. TPVS supports verification of temporal properties of reactive and concurrent systems described in terms of a Simple Programming Language (SPL). It uses PVS as a back-end. Boris Liberman's MSc Thesis is available.

University of York

O/S Verification, and User Interfaces

Simon Fowler is using PVS as part of work on the formal verification of real-time operating system kernels. The paper Formal Analysis of a Real-Time Kernel Specification was presented at FTRTFT'96, Uppsala, Sweden in September 1996, and represents the preliminary results of the work.

Nick Merriam is using PVS as part of a project investigating user interfaces to theorem provers. The paper Evaluating the Interfaces of Three Theorem Proving Assistants by Nick Merriam and Michael Harrison, presented at 3rd International Eurographics Workshop on Design, Specification, and Verification of Interactive Systems, Namur, Belgium, June 1996, describes initial work and considers the PVS interface as an example of the command line paradigm in the domain of theorem provers. The main thrust of the work is to use methods based on task analysis to evaluate interfaces to theorem provers and to make constructive design suggestions for improving task support.

Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Thu 30 Nov 2006 12:16 UTC
Maintainer: Sam Owre