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
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.
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 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.
Ulrich Hensel (with Bart Jacobs of Nijmegen) has been using PVS in formalizing coalgebraic datatypes (such as sequences) and their proof principles.
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.
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.
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.
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.
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)
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).
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).
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.
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)
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
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.
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.
A group in the Dipartimento di Elettronica e Informazione at the Politecnico di Milano is using PVS to support mechanized analysis of TRIO specifications.
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
Bart Jacobs has been using PVS in formalizing coalgebraic datatypes (such as sequences)
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.
Rick Butler provides An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot in NASA Technical Memorandum 110255 of May 1996.
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
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.