The ORA Canada Bibliography

Note:This material is presented for the dissemination of technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Year: 1999, 1998, 1997, 1996, 1995, 1994, 1993, 1992, 1991, 1990

1999

Formal Methods Adoption: What's working, What's not!.
Dan Craigen. ORA Canada, September 1999. Invited presentation for 6th International SPIN Workshop on Practical Aspects of Model Checking. To appear in Theoretical and Practical Aspects of Automata-based Model Checking: Proceedings of the 5th and 6th SPIN Workshops. Stefan Leue, et al., editors. Available through Springer-Verlag LNCS series.

Drawing from the author's twenty years of experience in formal methods research and development, and, particularly, with the EVES-based systems, this paper provides personal impressions on what is and what is not working with regards to the adoption and application of formal methods. As both the community's understanding of technology transfer issues and formal methods technology improve, one is optimistic that formal methods will play an increasingly important role in industry. However, significant impediments continue to exist with, perhaps, the increasing complexity of systems being both a blessing and a curse.

Analysing Z Specifications with Z/EVES.
Dan Craigen, Irwin Meisels, and Mark Saaltink. In Industrial-Strength Formal Methods in Practice, J.P. Bowen and M.G. Hinchey (Editors), September 1999. Available through Springer-Verlag FACIT series.

This paper illustrates the use of the Z notation in a formal specification (of the Sliding Window protocol), and shows how Z/EVES can be used to analyse and validate the specification.

Experience with Formal Methods in Critical Systems.
S. Gerhart, D. Craigen and T. Ralston. IEEE Software, January 1994. (17 pages) Reprinted in High-Integrity System Specification and Design, J.P. Bowen and M.G. Hinchey (Editors), April 1999. Available through Springer-Verlag FACIT series.

Although there are indisputable benefits to society from the introduction of computers into everyday life, some applications are inherently risky. Worldwide, regulatory agencies are examining how to assure safety and security. This study reveals applicability and limitations of formal methods.

OKBC API for Ontolingua.
Sentot Kromodimoeljo. ORA Canada, April 1999.
TR-99-5536-03. Not available for distribution at present.

This report describes the Application Program Interface (API) for Ontolingua version 4.0 that conforms to the proposed Open Knowledge Base Connectivity (OKBC) protocol version 2.02. The API provides access to knowledge bases implemented using generic frames within Ontolingua. A listing of supported OKBC calls is provided.

Integration of Z/EVES and Ontolingua.
Mark Saaltink. ORA Canada, April 1999.
TR-99-5536-04. Not available for distribution at present.

This report describes the integration of Ontolingua and Z/EVES. The integration allows Z specifications to be presented in Ontolingua's notation; allows functions that compute Z terms to be defined, and allows Z/EVES to be invoked to operate on parts of a specification. The integration is mediated by the use of an executable subset of KIF. We use KIF because it is the language of choice for Ontolingua, and is used to explain the meaning of Ontolingua ontologies.

Ontolingua to ExESS Translator.
Irwin Meisels. ORA Canada, April 1999.
TR-99-5536-05. Not available for distribution at present.

This document describes how to install and use the Ontolingua to ExESS translator, developed as part of the Ironman V1.5 project by ORA Canada. The translator extracts class, slot, and instance information from an Ontolingua ontology, and uses this information to generate ExESS frame and generic attribute (GAF) definitions and assertions which create an ExESS knowledge base.

KIF to CLIPS Translator.
Sentot Kromodimoeljo. ORA Canada, March 1999.
TR-99-5536-02. Not available for distribution at present.

This report describes the porting and validation of the CLIPS translation tool in Ontolingua version 4.0 to the environment for IRONMAN V1.5. Since the porting of Ontolingua itself is a separate task, the report focuses on the validation. General observations about the translator, as well as errors in the translator are discussed. This reort concludes with a discussion of a possible interface with CLIPS.

Using CSP Processes to Annotate and Prove Sequential Procedures.
Mark Saaltink. ORA Canada, February 1999.
ASSIGN NUMBER

This paper describes how CSP processes can be used to annotate sequential procedures that perform input and output operations, and how these annotations can be formally verified using the Floyd-Hoare method. The method is described informally, but has also been applied within a rigorous verification system.

A Prototype Protocol Analyser.
Mark Saaltink. ORA Canada, January 1999.
TR-98-5531-05

This report describes how to use a prototype protocol analyser that implements the approach described by Debbabi, et al.

1998

An Assessment of Tools for the Analysis of Authentication Protocols.
Mark Saaltink and Irwin Meisels. ORA Canada, December 1998.
TR-98-5531-02. Not available for distribution at present.

In this report we provide a preliminary assessment of several tools for the analysis of authentication protocols. The tools examined are DYMNA, a specialized protocol analyser; FDR2, a tool for verifying refinement relations between CSP processes, with a front end (Casper) for analysing protocols; AAPA, the Automatic Authentication Protocol Analyser, which supports a modal logic; EVES and Z/EVES, general theorem provers; and Murphi, a model checker.

Analysing Authentication Protocols.
Mark Saaltink and Irwin Meisels. ORA Canada, December 1998.
TR-98-5531-03. Not available for distribution at present.

This report describes how several tools (AAPA, Casper/FDR2, Dymna, and Z/EVES) can be used to analyse authentication protocols. After discussing the general issues to be considered and the overall approach, it is shown how a simple protocol (the Needham-Schroeder Public Key Protocol) and a commercial protocol can be analysed in each of the systems.

1997

Domain Checking Z Specifications.
Mark Saaltink. ORA Canada, accepted for the 4th NASA LaRC, Formal Methods Workshop, September 1997. (10 pages)
CP-97-6018-65.dvi
CP-97-6018-65.ps

We describe how guards can be used to ensure that formulas in a partial logic are meaningful, and how guards and guarded formulas can be proved using classical logic. In addition to this theoretical utility, guards are useful in practice as a simple means of exposing flaws in specifications. We illustrate this use of guards with several examples in the Z specification language, using Z/EVES.

The Z/EVES Reference Manual.
Mark Saaltink and Irwin Meisels. ORA Canada, December 1995; revised September 1997. (approx. 104 pages)
TR-97-5493-03d.dvi
TR-97-5493-03d.ps

Z/EVES is a tool for parsing, type checking, well-definedness checking, and proving theorems about Z specifications. This reference manual describes the Z syntax accepted by Z/EVES; the system and prover commands and their effects; the different types of theorems that can be expressed; and the Z/EVES version of the Mathematical Toolkit. Before getting to those details, we begin with a description of a short session with Z/EVES that illustrates some of its capabilities.

The Z/EVES Mathematical Toolkit for Z/EVES, Version 1.5
Mark Saaltink. ORA Canada, revised September 1997.
TR-97-5493-05a.dvi
TR-97-5493-05a.dvi

Abstract to be added.

The Z/EVES User's Guide
Mark Saaltink. ORA Canada, September 1997.
TR-97-5493-06.dvi
TR-97-5493-06.ps

Abstract to be added.

Z/EVES Reference Sheet.
Irwin Meisels. ORA Canada, September 1997. (2 pages)
TR-97-5493-07.dvi
TR-97-5493-07.ps

A two-page summary of the commands for using the Z/EVES system.

Software Manual for Windows Z/EVES Version 1.5 and the Z Browser.
Irwin Meisels. ORA Canada, January 1996; revised September 1997. (10 pages)
TR-97-5505-04e.dvi
TR-97-5505-04e.ps

This document describes the procedure for installing Version 1.5 of the Z/EVES verification system on a Windows 3.1 system or Windows 95 system.

Software Manual for Unix Z/EVES Version 1.5.
Irwin Meisels. ORA Canada, June 1996; revised September 1997. (5 pages)
TR-97-6028-01c.dvi
TR-97-6028-01c.ps

This document describes the procedure for installing Version 1.5 of the Z/EVES verification system on a SunOS 4.x or Linux system.

The Z/EVES System
Mark Saaltink. ORA Canada, In ZUM'97: The Z Formal Specification Notation (10th International Conference of Z Users, Reading, UK, April 1997, Proceedings), Lecture Notes in Computer Science 1212, Jonathan P. Bowen, Michael G. Hinchey and David Till (Eds.), Springer-Verlag, Berlin, pages 72-85. (14 pages)
CP-96-6018-64.dvi
CP-96-6018-64.ps

We describe the Z/EVES system, which allows Z specifications to be analysed in a number of different ways. Among the significant features of Z/EVES are domain checking, which ensures that a specification is meaningful, and a theorem prover that includes a decision procedure for simple arithmetic and a heuristic rewriting mechanism that recognizes "obvious" facts.

Ada 95 Trustworthiness Study: Analysis of Ada95 for Critical Systems (Version 2.0)
Mark Saaltink (ORA Canada) and Steve Michell (Maurya Software). March 1997. (326 pages)
TR-97-5499-03a.ps (Part 1)
TR-97-5499-03a.ps (Part 2)

This report describes an analysis of the applicability of Ada95 for use as the programming language in the development of critical systems.

Guidance on the Use of Ada95 in the Development of High Integrity Systems, Version 1.0
Mark Saaltink (ORA Canada) and Steve Michell (Maurya Software). March 1997. (101 pages)
TR-97-5499-04a.

This report gives guidelines for the use of Ada95 in the development of high integrity systems.

Reverse Engineering the CSP Y-Trap
Dan Craigen. ORA Canada, March 1997. (3 pages)
TR-97-5501-17. Not available for distribution at present.

This report is an "umbrella document" that ties together the analyses that have been performed by ORA Canada and AEPOS Technologies on the CSP Y-Trap, as part of our work for "Reverse Engineering the Standard Interface Device."

Low-Level Formalization of the CSP Y-Trap
Sentot Kromodimoeljo. ORA Canada, March 1997. (46 pages)
TR-97-5501-15. Not available for distribution at present.

This document describes the steps involved in our low-level formalization of the CSP Y-Trap.

Reverse Engineering Final Report
Dan Craigen. ORA Canada, March 1997. (16 pages)
TR-97-5501-14. Not available for distribution at present.

This final report summarizes our experiences from developing a formal methods-based reverse engineering methodology and its use on two applications of the Strategic Message Switching System Interface Device (SID) family: Mill Cove and the CSP Y-Trap.

Reverse Engineering Mill Cove
Dan Craigen. ORA Canada, March 1997. (4 pages)
TR-96-5501-12. Not available for distribution at present.

This report is an "umbrella document" that ties together the analyses that have been performed by ORA Canada and AEPOS Technologies on Mill Cove, as part of our work for "Reverse Engineering the Standard Interface Device."

Revised Low Level Specifications
J. David Andrews (AEPOS) and Mark Saaltink (ORA Canada). ORA Canada, March 1997. (5 pages)
TR-97-5501-11. Not available for distribution at present.

This report describes the use of a formal methods-based reverse engineering methodology for attaining high assurance of legacy systems on an application of the Strategic Message Switching System Interface Device (SID) family: Mill Cove.

The Original Low Level Specification For Mill Cove
J. David Andrews (AEPOS), Mark Saaltink (ORA Canada). ORA Canada, March 1997. (8 pages)
TR-97-5501-10. Not available for distribution at present.

This report discusses a problem in relating different abstract descriptions of an application of the Strategic Message Switching System Interface Device (SID) family: Mill Cove. The problem resulted in an inconsistency between our abstractions. We suggest possible solutions to the problem, one of which was used to successfully model Mill Cove.

The SID Architecture Formal Model
Sentot Kromodimoeljo, Irwin Meisels, and Mark Saaltink. ORA Canada, March 1997. (165 pages)
TR-97-5501-08. Not available for distribution at present.

This report describes a formal model, using Verdi and EVES, of the underlying hardware for the Strategic Message Switching System Interface Device (SID) family of terminal controllers. SID applications run on a standardized hardware configuration with a Z80 processor. The Verdi formal model, the EVES system, and a tool for translating Z80 code to Verdi, provide an infrastructure for proving properties of SID programs.

Modelling the Z80 in EVES
Mark Saaltink. ORA Canada, March 1997. (19 pages)
TR-97-5501-03. Not available for distribution at present.

This report describes a formal model, using Verdi and EVES, of the Z80 architecture, and shows how this model can be used to prove facts about Z80 programs. The techniques described here apply generally to the problem of modelling assembly language programs on any hardware platform.

1996

Reference Manual for the Language s-Verdi.
Dan Craigen, with contributions from Sentot Kromodimoeljo, Irwin Meisels, Bill Pase and Mark Saaltink, ORA Canada, February 1996; revised December 1996. (218 pages)
TR-96-5482-08a.dvi
TR-96-5482-08a.ps

This document presents an informal description of the language s-Verdi. Using the alternative syntax, s-Verdi is an interface language with the EVES verification system and consists of components for specifying and implementing programs, for proving consistency between specification and implementation, and for supporting miscellaneous other system capabilities.

Software Manual for Windows EVES Version 3.0.
Irwin Meisels. ORA Canada, January 1996; revised October 1996 (8 pages).
TR-96-5505-03a.dvi
TR-96-5505-03a.ps

This document describes the procedure for installing Version 3.0 of the EVES verification system on a Windows 3.1 system.

Using EVES to analyze authentication protocols.
Dan Craigen and Mark Saaltink. ORA Canada, March 1996. (44 pages)
TR-96-5508-05.dvi
TR-96-5508-05.ps

We have been experimenting with embedding an Authentication Logic into EVES. Specifically, we investigated the mechanization of a belief logic developed by Burrows, Abadi and Needham (the "BAN Logic"). After introducing the BAN Logic, we discuss our embedding of the BAN Logic into EVES. We then analyze three authentication protocols: Kerberos, CCITT X.509, and an idealized authentication protocol for the One Way Link. Next, improvements to our heuristics, associated with the EVES embedding of the BAN Logic, are made so that the proofs are more automatic. We demonstrate the improvements on the Kerberos Protocol. An alternative approach to mechanizing the Authentication Logic and the example protocols is then presented. The alternative approach provides substantially improved automatic analysis. Finally, we discuss issues pertaining to the soundness and completeness of the BAN Logic and provide some conclusions.

The one way link system/subsystem design description.
Sentot Kromodimoeljo. ORA Canada, March 1996. (168 pages, including listings)
TR-96-5508-04.dvi
TR-96-5508-04.ps

This System/Subsystem Design Description contains the architectural and detailed designs for the One Way Link prototype. As required by the contract, the designs are formalized in s-Verdi, with proofs of correspondence between different levels of formalization. The architectural design is described in terms of Communicating Sequential Processes.

The one way link system/subsystem specification.
Sentot Kromodimoeljo. ORA Canada, March 1996. (16 pages)
TR-96-5508-03.dvi
TR-96-5508-03.ps

This System/Subsystem Specification contains the functional specification for the One Way Link (OWL) prototype. As required by the contract, this document includes the security policy for OWL; formalization of the security policy, in the form of a security policy model written in s-Verdi; and a preliminary covert channel analysis.

Report on Z/EVES and the Z Browser.
Irwin Meisels. ORA Canada, March 1996. (6 pages)
TR-96-5505-06.dvi
TR-96-5505-06.ps

This document reports our experiences in linking Z/EVES and the Z Browser. It describes the ways we considered of linking the two programs, problems encountered, experiences using the two programs, and gives some suggestions for future work.

Linking Data Flow Diagrams to EVES.
William Pase. ORA Canada, March 1996. (42 pages)
TR-96-5505-05.dvi
TR-96-5505-05.ps

The principle purpose of this study was to link an existing Graphical User Interface with EVES, thus completing a GUI tool for security modelling with EVES. The work reported here furthers the results of previous efforts by ORA Canada on behalf of the Communications Security Establishment.

Ada95 and Critical Systems: An Analytical Approach.
Dan Craigen, Mark Saaltink and Steve Michell (Maurya Software). In Proceedings of the "Ada-Europe 96 Conference", February 1996. (12 pages)
ORA Canada's number:
CP-96-6018-61.dvi
CP-96-6018-61.ps

In this paper, we discuss how the suitability of Ada95 for use in critical systems is being assessed. We will describe our framework and provide examples of assessing specific Ada constructs within the terms of the framework.

Reference Manual for the Language Verdi.
Dan Craigen. ORA Canada, June 1995; revised February 1996. (168 pages) Formerly TR-95-5429-09c.
TR-96-5482-07.dvi
TR-96-5482-07.ps

This document presents an informal description of the language Verdi. Verdi is the interface language with the EVES Version 2.5 verification system and consists of components for specifying and implementing programs, for proving consistency between specification and implementation, and for supporting miscellaneous other system capabilities.

EVES Quick Reference [using s-Verdi].
Mark Saaltink, ORA Canada, February 1996. (8 pages)

Presented as a pamphlet, this is a pocket-size guide to the language s-Verdi.

Process approach for the development of high assurance one way link.
Sentot Kromodimoeljo. ORA Canada, January 1996. (5 pages)
WP-96-5508-02.dvi
WP-96-5508-02.ps

In this working paper, we describe our approach in developing a design of a communications device called the One Way Link (OWL). We identify the relevant sections of MIL-STD-498 and CTCPEC throughout the description.

1995

A Tutorial on EVES using s-Verdi.
Sentot Kromodimoeljo, Bill Pase, Mark Saaltink, Dan Craigen and Irwin Meisels. ORA Canada, December 1995.
TR-95-6018-60.dvi
TR-95-6018-60.ps

This paper provides a tutorial introduction to EVES. EVES is a formal methods tool consisting of a set theoretic-based language, called Verdi, and an automated deduction system, called NEVER. We provide a general introduction to EVES and demonstrate its capabilities using (i) some examples from set theory, (ii) a small critical application (a railroad crossing), and (iii) a small program proof.

EVES Proof Checking and Browsing Final Report.
Sentot Kromodimoeljo, Bill Pase, and Mark Saaltink. ORA Canada, December 1995. (14 pages)
TR-95-5482-06.dvi
TR-95-5482-06.ps

This final report summarizes our work on EVES Proof Checking and Browsing, performed for the Department of National Defence under contract number W2207-3-AF16/01-SV. We report on our experiences while completing the development of the EVES mathematics, developing a prototype stand-alone proof checker, and developing a prototype browsing capability.

Installation Guide for PC EVES Version 3.0.
Irwin Meisels. ORA Canada, December 1995. (4 pages).
TR-95-5482-05.dvi
TR-95-5482-05.ps

PC EVES is a version of the EVES verification system which runs on PCs under the DOS operating system. It has been built with a version of Kyoto Common Lisp (KCL) which was ported to DOS using Eberhard Mattes' EMX port of GNU C. This document describes how to install and use PC EVES.

Prototype Proof Checker.
Bill Pase and Sentot Kromodimoeljo. ORA Canada, December 1995. (3 pages)
TR-95-5482-04.dvi
TR-95-5482-04.ps

The Proof Checking and Browsing effort was an attempt to develop the actual assurance tools that use the proof logs. A prototype stand-alone proof checker and a preliminary proof browser were developed during this effort. This report is a brief user's guide to the prototype proof checker.

Software Manual for EVES Version 3.0.
Sentot Kromodimoeljo, Bill Pase and Irwin Meisels. ORA Canada, December 1995. (7 pages)
TR-95-5482-03.dvi
TR-95-5482-03.ps

This document describes the procedure for installing Version 3.0 of the EVES verification system on a Unix system.

Z/EVES summary paper.
Mark Saaltink and Irwin Meisels. ORA Canada, December 1995. (7 pages)
TR-95-5493-04.dvi
TR-95-5493-04.ps

This report summarizes the work performed for the Z/EVES contract. Each of the tasks are briefly described, and the conclusions and recommendations are itemized.

Ada95 Trustworthiness Study: A Framework for Analysis.
Dan Craigen, Mark Saaltink and Steve Michell (Maurya Software). ORA Canada, November 1995. (57 pages)
TR-95-5499-02.ps

This report describes the framework to be used in analysing Ada95 for use on critical applications, and the reasons for establishing such a framework. This work was done in concert with the Safety and Security Rapporteur Group of the International Ada Working Group, otherwise known simply as the "HRG". The work was funded by the Canadian Department of National Defence.

The EVES Library.
Mark Saaltink. ORA Canada, October 1995. (104 pages)
TR-95-5449-03a.dvi
TR-95-5449-03a.ps

This report documents the library units contained in the standard EVES library. All the units have fully proven models. The Verdi text for the specifications and models can be found in the standard EVES examples directory.

Trip report: QED Workshop II, Warsaw, Poland, July 20-22, 1995.
Bill Pase. ORA Canada, September 1995. (8 pages)
TR-95-5505-02.dvi
TR-95-5505-02.ps

This note reports on the QED Workshop II, held in Warsaw, Poland, July 20-22, 1995. The workshop was hosted by Warsaw University, Bialystok Branch (Mizar Group), under the auspices of the State Committee for Scientific Research (Poland), co-sponsored by the Office of Naval Research (USA), and Microsoft (Poland).

Formal Methods Technology Transfer: Impediments and Innovation.
Dan Craigen and Susan Gerhart and Ted Ralston.
In Applications of Formal Methods. ed. M. G. Hinchey and J. P. Bowen. Prentice-Hall International Series in Computer Science, September 1995. (23 pages)

An innovation diffusion model is used to analyze the data collected during an international survey of industrial applications of formal methods. The model provides a structured means for determining the likely adoption trajectory of formal methods. We conclude that formal methods will only be slowly diffused into industry and provide examples and recommendations on how to ease impediments to diffusion.

EVES Quick Reference [using Verdi].
ORA Canada, June 1995. (6 pages)

A summary of EVES (using Verdi) declarations, prover commands, and command modifiers; and a one page summary for the GNU Emacs Interface.

Proof Logging Final Report.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, June 1995. (6 pages)
TR-95-5471-05.dvi
TR-95-5471-05.ps

This report is the final report for proof logs in NEVER, as they appear in EVES, version 2.4.2. It describes the design of proof logging, and the difficulties encountered during the contract "Proof Logging Tool Development" (W2207-2-AF08/01-SV).

Proof Logging User Manual.
Bill Pase and Sentot Kromodimoeljo. ORA Canada, June 1995. (4 pages)
TR-95-5471-04.dvi
TR-95-5471-04.ps

This report is the user manual for proof logs in NEVER, as they appear in EVES, version 2.4.2. It describes how to use the proof logging tool.

Towards a formal semantics for Ada9X.
D. Guaspari and J. McHugh and W. Polak and Mark Saaltink. NASA contractor report 195037, March 1995. (ORA Canada TR-95-5484-02) (150 pages)

The Ada 9X Language Precision Team (LPT) was formed in 1990 to study portions of the design of Ada 9X from a mathematical perspective. The first LPT project studied small parts of the language in isolation, formulating fairly simple models to explore the ramifications of the design. The results were reported previously.

The second LPT project had two separate goals: to study the rules of allowed optimizations; and to formulate a broad model to cover a large part of the language. The resulting model and experiences from the project are reported in this document.

A Formal Description of Verdi.
Mark Saaltink. ORA Canada, TR-95-5482-02, March 1995. (108 pages)
TR-94-5429-10b.dvi
TR-94-5429-10b.ps

This report gives a precise formal description of Verdi (to the level of abstract syntax) and defines the proof obligations that must be proved to demonstrate that a program is in consonance with its specifications. A model theory (semantics) of the language is defined and used to show the adequacy of the proof obligations. (Released October 1989, revised August 1994 as TR-94-5429-10b.)

The Role of Education and Training in the Industrial Application of Formal Methods.
Susan Gerhart, Ted Ralston and Dan Craigen. In Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST'95), Lecture Notes in Computer Science, Springer-Verlag, 1995.

During two one-year studies, data was collected on education and training background and requirements for the successful transfer of formal methods to industry. This paper reports our observations and conclusions from both studies. One of the primary purposes of the second study was to provide a more systematic record of industrial experiences on a number of alleged deficiencies in the application of formal methods. One of these deficiencies is the contention that formal methods require prodigious mathematical education and talent for their successful use. Our interviews explored such issues as in-house company education; external education; differences in curricula between North America and Europe; profiles of personnel working on formal methods projects; and the role of tools as educational media.

Application of EVES to Reverse Engineering Software.
Dan Craigen. ORA Canada, March 1995. (46 pages)
FR-95-5476-02.dvi
FR-95-5476-02.ps

The intent of the contract was to build upon previous ORA Canada internal research and development on using EVES on a small C encoded encryption program, by further exploring the reverse engineering literature, and providing (if possible) a generic reverse engineering strategy based on EVES. This paper consists of a discussion of terminology and various reverse engineering articles; a discussion of previous experiences with formal methods and reverse engineering; a detailed discussion of our first application of EVES to a reverse engineering application; a discussion of two possible approaches for using EVES to reverse engineer assembler programs; a general discussion of possible uses of EVES to reverse engineer legacy code; and the conclusions.

Developing a theory of Information Flow Algebras in EVES.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, March 1995. (26 pages)
TR-95-5492-03.dvi
TR-95-5492-03.ps

This report describes our work on developing an EVES theory for portions of Information Flow Algebras (IFAs). The Information Flow Algebra approach is an algebraic framework being developed at CGI to model information flow in computer systems. The motivation behind using IFA as a framework is the observation that aggregations and compositions of abstract flows resemble sums and products, respectively.

Ontological GUI and EVES.
Sentot Kromodimoeljo, ORA Canada, March 1995. (6 pages)
TR-95-5492-04.dvi
TR-95-5492-04.ps

The effort reported here attempts to bring us closer towards the goal of having a GUI for EVES. In this report, we give an overview of the IDEF1X standard, discuss possible translations of IDEF1X formalization to EVES, and discuss the results of our investigation on the possible roles of IDEF1X. Although the main focus of the effort was on the formal aspects of a GUI, we also investigated some of the pragmatic issues concerning the glue between EVES and a GUI on a PC platform running DOS. We briefly discuss the results of this investigation.

Formal Methods Reality Check: Industrial Usage.
Dan Craigen, Susan Gerhart and Ted Ralston.
IEEE Transactions on Software Engineering 21(2):90-98, February 1995.
Also in Proceedings of "Formal Methods Europe'93" (FME'93, Odense, Denmark), Springer-Verlag, April 1993.

Based on a systematic survey and analysis of the use of formal methods in the development of a dozen industrial applications, we summarize the methods being used, characterize the styles of industrial usage, and provide recommendations for evolutionary enhancements to the technology base of formal methods.

The industrial applications ranged from reverse engineering to system certification; code scale ranges from 1 KLOC to 10 KLOCs. Applications included a software infrastructure for oscilloscopes, a shutdown system for a nuclear generating station, a train protection system, an airline collision avoidance system, an engine monitoring system for shipboard engines, attitude control of satellites, security properties of both a smartcard device and a network, arithmetic units, transaction processing, a real-time database for a medical instrument, and a restructuring program for COBOL. Previously CP-93-6017-50.

An International Survey of Industrial Applications of Formal Methods.
Dan Craigen and Susan Gerhart and Ted Ralston.
NIST GCR 93/626 (Volumes 1 and 2), U.S. National Institute of Standards and Technology, March 1993. Also published by the U.S. Naval Research Laboratory (Formal Report 5546-93-9582, September 1993), and the Atomic Energy Control Board of Canada, January 1995.
NIST GCR 93/626, Vol 1 (postscript only)
NIST GCR 93/626, Vol 2 (postscript only)

1994

Installation Guide for PC EVES Version 2.3.
Irwin Meisels. ORA Canada, September 1994. (4 pages)
TR-94-5492-02.dvi
TR-94-5492-02.ps

PC EVES is a version of the EVES verification system which runs on PC's under the DOS operating system. It has been built with a version of Kyoto Common Lisp (KCL) which was ported to DOS using Eberhard Mattes' EMX port of GNU C. This document describes how to install and use PC EVES.

Using EVES to analyse SCR-style specifications.
Mark Saaltink. ORA Canada, September 1994. (51 pages)
TR-94-5490-02.dvi

The purpose of this project was to assess the utility of EVES as a tool for analysing SCR-style specifications. Specifically, we wanted to experiment with the transcription of SCR-style tabular specifications into Verdi, the generation of completeness and consistency conditions, and the use of EVES to prove the conditions, symbolically execute the specified system, and prove simple safety properties.

A Tutorial on EVES.
Sentot Kromodimoeljo, Bill Pase, Mark Saaltink, Dan Craigen and Irwin Meisels. ORA Canada, September 1994. (45 pages)
CP-94-6017-51.dvi

This paper provides a tutorial introduction to EVES. EVES is a formal methods tool consisting of a set theoretic-based language, called Verdi, and an automated deduction system, called NEVER. We provide a general introduction to EVES and demonstrate its capabilities using an example of data abstraction (table/list), a small hardware example (an adder), and a small critical application (a railroad crossing).

Mapping Verdi Concrete Syntax to Abstract Syntax.
Mark Saaltink. ORA Canada, August 1994. (10 pages)
TR-94-5463-07.dvi
TR-94-5463-07.ps

This document formally describes the mapping from Verdi's concrete syntax, as described in the Reference Manual, to the abstract syntax used in the formal definitions.

A four-phase translation from Verdi to Intermediate Language.
Mark Saaltink. ORA Canada, August 1994. (23 pages)
TR-94-5463-05.dvi
TR-94-5463-05.ps

This report defines a translation from Verdi abstract syntax to Intermediate Language. This translation applies only to a subset of Verdi. This subset eliminates all non-manifest types. In particular, open-array parameters are not allowed, and all type expressions must be manifest. Four steps are used in the translation from Verdi to Intermediate Language. We will briefly describe the steps here.

Verdi Compiler: Final Report.
Mark Saaltink and Irwin Meisels. ORA Canada, July 1994. (17 pages)
TR-94-5463-13.dvi
TR-94-5463-13.ps

The Verdi compiler project had the goal of building a Verdi compiler with two parts: one mapping from Verdi to some intermediate language, the other mapping the intermediate language to assembly language or machine code for some target. The first part, which is almost completely independent of the target, was to have its translation mathematically justified.

This report describes the results of the work on the tasks involved in completing this contract. A detailed description of the structure of the Verdi compiler, and the relation between its implementation to the formal specifications of its tasks, is presented in Structure of the SPARC Verdi Compiler.

Translating Verdi Intermediate Language into SPARC Code.
Irwin Meisels. ORA Canada, July 1994. (50 pages)
TR-94-5463-12.dvi
TR-94-5463-12.ps

This paper specifies the translation of Verdi intermediate language (IL) into code for the SPARC architecture. The IL in this document is an abstract version of the IL described in Structure of the SPARC Verdi Compiler, in which no distinction is made between operator attributes and operands.

The Lexical Structure of Verdi.
Mark Saaltink. ORA Canada, July 1994. (6 pages)
TR-94-5463-06.dvi
TR-94-5463-06.ps

This report formally defines the lexical structure of Verdi, using the Z notation. This formulation of lexical structure is similar to the definition in the formal definition of Turing.

The grammar of Verdi, like that of most programming languages, is most conveniently described using two distinct phases: lexical analysis and parsing. Verdi programs are composed of characters. Lexical analysis transforms this sequence of characters to a sequence of tokens. This sequence of tokens is then parsed according to a context-free grammar.

Structure of the SPARC Verdi Compiler.
Irwin Meisels. ORA Canada, June 1994. (37 pages)
TR-94-5463-11.dvi
TR-94-5463-11.ps

This document describes the structure of the SPARC Verdi compiler. The development of this compiler was more "rigorous" than most: there are formal specifications for each pass of the compiler, and a proof that the semantics of a Verdi program (for a subset of Verdi) are "congruent" with those of the generated intermediate language.

In describing the structure of the compiler, this document also relates the passes to the specifications.

SPARC Verdi Compiler User's Manual.
Irwin Meisels. ORA Canada, June 1994. (16 pages)
TR-94-5463-10.dvi
TR-94-5463-10.ps

This document describes how to install and use the SPARC Verdi compiler, version 1.0. The compiler runs on and generates code for Sun computers using the SPARC processor and running SunOS version 4.1.1 and above. The compiler does not yet run under Solaris.

The Semantics of the Verdi Intermediate Language.
Mark Saaltink. ORA Canada, April 1994. (21 pages)
TR-94-5463-08.dvi
TR-94-5463-08.ps

This report describes the semantics of the Verdi Intermediate Language (IL). Defining the semantics of the Intermediate Language proved to be more difficult that we had originally thought. Several factors combined to make the definition difficult, but foremost among them was machine-independence. Because the IL is intended to allow for code generation for a wide variety of machine architectures and calling conventions, many of its details are loosely defined.

An Alternative Syntax for Verdi.
Irwin Meisels. ORA Canada, April 1994. (28 pages)
TR-94-5478-02.dvi
TR-94-5478-02.ps

This document describes an alternative syntax for Verdi. The design for this syntax had the following goals: the new syntax should be closer to what people are used to (Pascal or Ada-like declarations and infix expression syntax); the new syntax should be easily transliterated into Verdi syntax, and vice versa; and the new expression syntax should be flexible. This document presents the lexical and syntactic structure of the new syntax, and shows how the transliteration to Verdi is done.

Adding Front-ends to EVES.
Irwin Meisels. ORA Canada, March 1994. (48 pages)
TR-94-5478-03.dvi
TR-94-5478-03.ps

This document describes a standardized interface to EVES which allows front-ends to be added easily. One example is a front-end which accepts a Pascal-style syntax, with expressions in a user-extensible infix notation, and prints results in the same syntax. Other possibilities include a front-end which uses a windowing system and graphical interface, and a front-end which runs on one machine and communicates with an EVES process running on another.

Formal Methods, EVES, and Safety Critical Systems.
Dan Craigen. ORA Canada, January 1994. (39 pages)
FR-94-5479-04.dvi
FR-94-5479-04.ps

While formal methods are a crucial technology in the development of safety- and security-critical systems, their relationship to safety analysis techniques has received limited attention. The results of our safety analysis literature review and interviews with researchers and practitioners, and recommendations and observations of the synergism between formal methods and safety analysis, are presented in this report.

Experience with Formal Methods in Critical Systems.
S. Gerhart, D. Craigen and T. Ralston. IEEE Software, January 1994. (17 pages)

Although there are indisputable benefits to society from the introduction of computers into everyday life, some applications are inherently risky. Worldwide, regulatory agencies are examining how to assure safety and security. This study reveals applicability and limitations of formal methods.

1993

Using triggered axioms to build decision procedures. In `Addendum to the "Final Report for the Investigation of Proof Techniques Within the EVES Verification Technology".'
Mark Saaltink. ORA Canada, December 1993. (12 pages)
TR-93-5451-03.dvi
TR-93-5451-03.ps

We describe a triggering mechanism that can be used to build decision procedures for some theories. The main result gives a condition that guarantees that a particular set of triggered axioms can be applied by the method to decide a theory.

The Knuth-Bendix Implementation. In `Addendum to the "Final Report for the Investigation of Proof Techniques Within the EVES Verification Technology".
Sentot Kromodimoeljo and Bill Pase. ORA Canada, December 1993. (3 pages)
TR-93-5451-03.dvi
TR-93-5451-03.ps

An implementation of the Knuth-Bendix algorithm has been added to EVES. The variation of the algorithm chosen allows analysis of both unconditional and conditional equations. Thus, the algorithm, which deals with conditional equations, is expected to be more useful within EVES than the original algorithm described by Knuth-Bendix.

Security Modelling Using EVES.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, December 1993. (71 pages)
TR-93-5479-02.dvi
TR-93-5479-02.ps

This report describes the work on security modelling in EVES, performed for the Communications Security Establishment. We begin by briefly describe the ontological approach of architectural security modelling development at CSE, followed by our recommendations for the GUI requirements and the database requirements. We then describe the EVES interface to the security modelling tool and the cascade conditional analysis example as put through EVES. Finally, we conclude with some general observations and recommendations.

Translating structured commands to linear code.
Mark Saaltink. ORA Canada, October 1993. (10 pages)
TR-93-5463-04.dvi
TR-93-5463-04.ps

The final phase of the Verdi compiler translates a structured intermediate language into a sequence of instructions, jumps, conditional jumps, and (pseudo-)instructions that define labels.

This transformation can be defined and proved correct in a quite general setting. To that end, we define that transformation in terms of a syntax that includes some unspecified set of "primitive" commands, and a semantics that is based on some unspecified semantic functions.

A second alternative semantics for Verdi.
Mark Saaltink. ORA Canada, October 1993. (51 pages)
TR-93-5463-03.dvi
TR-93-5463-03.ps

In the course of the Verdi Compiler Verification project it has been necessary to revisit the Alternative Semantics and make some changes. The Verdi Compiler inserts code to check various legality conditions, such as overlap in parameter lists, indexing errors, arithmetic overflows, and type errors. These checks are clearly permitted by the model theory, which allows a program failing such a check to have an arbitrary outcome. So, in particular, such a program may terminate with a legality failure message.

The original definition of the alternative semantics did not permit these checks. In particular, the type checks were not allowed.

Fixed points in chain-completed partial orders.
Mark Saaltink. ORA Canada, October 1993. (6 pages)
TR-93-5463-02.dvi
TR-93-5463-02.ps

This report collects together the basic definitions and theorems about fixed points that are used in the analysis of Verdi. Much of the material here is collected from other reports, but there are also some new results needed in the analysis of the Verdi compiler.

Observations on Industrial Practice Using Formal Methods.
Susan Gerhart, Dan Craigen and Ted Ralston.
In Proceedings of the 15th International Conference on Software Engineering (ICSE'15), Baltimore, Maryland, May 1993.

"Formal Methods" refers to the use of mathematically based (specifically, logic-based) techniques in software and system engineering. This paper summarizes observations on the use of such techniques in a dozen applications in industrial settings. Application goals ranged from re-engineering to system certification; code scale ranges from 1000 LOC (for a complex safety-critical application through 10,000s LOC (for re-engineering coverage); applications include oscilloscopes, nuclear reactors, trains, planes, ships, satellites, smartcards, transaction processing, arithmetic units, networks, medical instruments, and language processors. The observations follow from a systematic survey and analysis of results using a structured interview process and a set of features for analyzing and assessing results. Observations cover various aspects of practice using formal methods: process, methods, tools, technology transfer, and evaluation of results. Previously CP-93-6017-52.

Formal methods are mathematically-based techniques, often supported by reasoning tools, that can offer a rigorous and effective way to model, design and analyze computer systems. The purpose of this study is to evaluate international industrial experience in using formal methods. The cases selected are, we believe, representative of industrial-grade projects and span a variety of application domains. The study had three main objectives: (i) to better inform deliberations within industry and government on standards and regulations; (ii) to provide an authoritative record on the practical experience of formal methods to date; and (iii) to suggest areas where future research and technology development are needed.

An EVES Data Abstraction Example.
Mark Saaltink, Sentot Kromodimoeljo, Bill Pase, Dan Craigen and Irwin Meisels.
In Proceedings of "Formal Methods Europe'93" (FME'93, Odense, Denmark), Springer-Verlag, April 1993.

This paper provides an introduction to EVES. EVES is a formal methods tool consisting of a language based on set theory, called Verdi, and an automated deduction system, called NEVER. We provide a general introduction to EVES and demonstrate its capabilities using an example of data abstraction (table/list).

1992

Investigating the Role of EVES in System Engineering and Security Evaluation.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, December 1992. (23 pages)
TR-92-5464-02.dvi
TR-92-5464-02.ps

The purpose of the work described here was to investigate the role of the EVES technology within the context of CSE needs for system assurance, and to develop a CSE-related application with EVES emphasizing how EVES was used for the development.

The EVES System.
Sentot Kromodimoeljo, Bill Pase, Mark Saaltink, Dan Craigen and Irwin Meisels.
In Proceedings of the International Lecture Series on "Functional Programming, Concurrency, Simulation and Automated Reasoning" (FPCSAR), McMaster University, August 1992. (22 pages)

After a brief introduction, we discuss two applications of EVES. The first application is a proof of Jacobson's Theorem. The second application is a proof of an interpreter for a small programming language; portions of the interpreter proof are described in this paper. We conclude by discussing some of the issues raised by the FPCSAR. Previously CP-92-6017-49.

Development of a skeletal CSP theory in EVES.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, July 1992. (41 pages)
TR-92-5469-02.dvi
TR-92-5469-02.ps

This report describes the development of a skeletal CSP theory in EVES. Various decisions in the development are explained, as are the motivations behind those decisions. A User's Guide to a Skeletal CSP Theory in EVES is the companion report to this work.

The work described in this report was funded by contract number N00014-92-P-2025, issued by the Naval Research Laboratory, Washington, DC, and administered by DCMAO Syracuse, NY.

A user's guide to a skeletal CSP theory in EVES.
Bill Pase and Sentot Kromodimoeljo. ORA Canada, July 1992. (36 pages)
TR-92-5469-03.dvi
TR-92-5469-03.ps

This report documents the EVES library units for the specification and proving of safety properties about systems composed of the CSP (communicating sequential processes) constructs. There are four specification units, plus their corresponding models, for a total of eight EVES library units. Together, these are intended to be sufficient for the development of specifications based upon CSP. This report describes the installation, contents, and use of these library units. Appendices provide the source for the complete specifications and examples. (Development of a Skeletal CSP Theory in EVES is the companion report to this work.).

The work described in this report was funded by contract number N00014-92-P-2025, issued by the Naval Research Laboratory, Washington, DC, and administered by DCMAO Syracuse, NY.

Final Report for the Investigation of Proof Techniques Within the EVES Verification Technology.
Sentot Kromodimoeljo and Bill Pase. ORA Canada, May 1992. (72 pages)
FR-92-5451-02.dvi
FR-92-5451-02.ps

This document reports on the work performed for the Canadian Department of National Defence under contract no. W2207-0-AF09/01-SV entitled "Investigation of Proof Techniques within the EVES Verification Technology". The purpose of this work was to research and experiment with various approaches for enhancing the capabilities of the theorem prover NEVER and, hence, the overall effectiveness of EVES.

An Introduction to EVES, Its Motivations, and Its Evolution.
Dan Craigen. ORA Canada, March 1992. (77 pages)
TR-92-5440-09.dvi
TR-92-5440-09.ps

This report presents background material for understanding the motives and directions of the EVES research and development program.

The report includes a discussion of formal methods and the role of EVES within the formal methods field, and a description of the proposed evolution of EVES. We conclude that there are significant potential applications of EVES in the development of critical systems.

Z and EVES: A summary.
Mark Saaltink. In Proceedings of the 6th Annual Z User Meeeting, 16 and 17 December 1991, Workshops in Computing, Springer-Verlag, Berlin, 1992. (20 pages)

ORA Canada has recently conducted a study with three primary goals: to assess the Z notation; to determine the feasibility of using EVES as a proof tool for Z; and to adapt the Z "Mathematical Toolkit" for use in EVES. In general, we would recommend the Z notation. We identified some difficulties in providing EVES support for Z, though we concluded that adding the Z Mathematical Toolkit to the EVES library will be useful to EVES users. Previously CP-91-6017-45.

Sharing is difficult.
Mark Saaltink, Dan Craigen, Sentot Kromodimoeljo and Bill Pase.
In Proceedings of TTCP-XTP-1 Workshop on effective use of automated reasoning technology in system development, April 1992. Previously CP-92-6017-47. (7 pages)

We paint a rather bleak and pessimistic picture of the prospects for sharing code or theorems between different proof tools. The problems arise in part because of the diverse logics and diverse methods used by the tools. We further argue that this diversity is not capricious, but is necessary as researchers explore different approaches to supporting formal reasoning.

Tool Support for Formal Methods.
Dan Craigen. In Proceedings of the 13th International Conference on Software Engineering, 1991. (2 pages)

Used as the basis of a presentation, this paper discusses the state of the art of formal methods tool support. Previously CP-91-6017-46.

EVES System Description.
D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase and M. Saaltink.
In Proceedings of CADE-11, Saratoga Springs, NY (June 1992), Springer-Verlag, New York, 1992. (5 pages)

A brief description of the Verdi language, concentrating on the EVES verification environment that has been implemented, particularly the theorem prover component. Previously ORA CP-91-6017-44.

1991

EVES: An Overview.
D. Craigen, S. Kromodimoeljo, I. Meisels, W. Pase and M. Saaltink.
In Proceedings of VDM '91 (Formal Software Development Methods), Noordwijkerhout, The Netherlands (October 1991), Lecture Notes in Computer Science 551, Springer-Verlag, Berlin, 1991. (5 pages)

In this paper we describe a new formal methods tool called EVES. EVES consists of a set theoretic language, called Verdi, and an automated deduction system, called NEVER. We present an overview of Verdi, NEVER, and the underlying mathematics; and develop a small program, to demonstrate the basic functionality of EVES. Previously CP-91-5402-43.

Z and EVES.
Mark Saaltink. ORA Canada, October 1991. (52 pages)
TR-91-5449-02.dvi
TR-91-5449-02.ps

This report begins with a short overview of Z for the benefit of readers who are unfamiliar with the notation. This is followed by the three main sections, corresponding to the three goals of the Z/EVES project: to assess the Z notation; to determine the feasibility of using EVES as a proof tool for Z; and to adapt to Z "Mathematical Toolkit" for use in EVES.

The EVES Library Models.
Mark Saaltink. ORA Canada, September 1991. (48 pages)
TR-91-5449-04.dvi
TR-91-5449-04.ps

This report lists the models for the library units contained in the standard EVES library (as it stood in 1991). The specifications of these library units are described in "The EVES Library" (TR-91-5449-03). The Verdi text for the specifications and models can be found in the standard EVES examples directory.

Verdi Interpreter User's Manual.
Irwin Meisels. ORA Canada, April 1991. (10 pages)
TR-91-5447-03.dvi
TR-91-5447-03.ps

This document describes the interpreter component of the EVES program verification system. Most of this report has been incorporated into the Verdi Reference Manual.

Proof Management: Final Report.
Sentot Kromodimoeljo, Bill Pase and Mark Saaltink. ORA Canada, January 1991. (33 pages)
FR-91-5445-02.dvi
FR-91-5445-02.ps

This final report summarizes the work completed for the project entitled Feasibility Study on the NEVER Theorem Prover (DSS Contract No. W2207-9-AF37/01-SV). The report places the contracted work within the context of the EVES project; outlines the project and the statement of work; summarizes the approach used to meet the contractual obligations; lists the documents and listings delivered at the termination of the project; and summarizes the results of the project.

Verification Environments.
Dan Craigen. In Software Engineers Reference Book, ed. John McDermid, Butterworths--Heinemann Ltd, 1991. (23 pages)

The classical structure of verification environments is described, and two examples show aspects of the m-EVES, Gypsy and Affirm environments. Previously CP-91-6017-48.

1990

Alternative Semantics for Verdi.
Mark Saaltink. ORA Canada, November 1990. (56 pages)
TR-90-5446-02.dvi
TR-90-5446-02.ps

This report complements the model theory by presenting an alternative definition of the semantics of the executable portion of Verdi, with a proof of correspondence between the new semantics and the old. The work was performed under funding from the Canadian Department of National Defence (Contract Number W2207-9-AF37/01-SV).

Simple Type Theory in EVES.
Dan Craigen and Mark Saaltink. In Proceedings of the Fourth Banff Higher Order Workshop, Graham Birtwistle, Springer-Verlag, New York" 1990. Previously ORA CP-90-5402-42.

This paper presents a brief description of a newly completed verification system called EVES. EVES is a formal system based on Zermelo-Fraenkel set theory with the Axiom of Choice. EVES supports the proof of mathematical properties, including proofs of program correctness. The development of EVES required the design of a new language, called Verdi, and of a heuristic theorem prover, called NEVER.

After introductory remarks on Verdi, NEVER and EVES, we present a combinatory version of Church's simple type theory in EVES as an illustration of the power and flexibility of the untyped set theory framework and of EVES.

Formal Methods for Trustworthy Computer Systems (FM'89).
Dan Craigen and Karen Summerskill. Springer-Verlag, 1990. (201 pages)

The 1989 Workshop on the Assessment of Formal Methods for Trustworthy Computer Systems (FM89) was an invitational workshop that brought together representatives from the research, commercial and governmental spheres of Canada, the United Kingdom, and the United States. The workshop was held in Halifax, Nova Scotia, Canada, from July 23 through July 27, 1989. This document reports the activities, observations, recommendations and conclusions resulting from FM89.

FM89: Assessment of Formal Methods for Trustworthy Computer Systems.
Dan Craigen. In Proceedings of the 12th International Conference on Software Engineering, Nice, France, April 1990.

FM89 was an invitational workshop that brought together representatives from the research, commercial and governmental spheres of Canada, the United Kingdom, and the United States. This article briefly describes the activities, observations, recommendations and conclusions of the workshop. Previously ORA CP-89-5402-40.

Final Report: Development of a Practical Computer Software Verification System.
Dan Craigen. ORA Canada, March 1990. (10 pages)
TR-90-5429-11.dvi
TR-90-5429-11.ps

This report presents an overview of research performed by ORA Canada for the Canadian Department of National Defence under contract W2207-7-AF78/01-SV.

Strengths and Weaknesses of Program Verification Systems.
Dan Craigen. In Proceedings of the 1st European Software Engineering Conference, Strasbourg, France (8-11 September 1987). (9 pages)

This paper discusses the putative strengths and weaknesses of the current generation of verification systems, the characteristics of a system which can be developed at low technical risk, and a research effort to develop a new verification system called EVES. Previously IPSA CP-87-5402-22, February 1987.

Some Comments on Program Verification Systems.
Dan Craigen. In Safe and Secure Computing Systems, Tom Anderson, Blackwell Scientific Publications, 1989.

Position paper for Symposium on Safety and Security (20-24 October 1986), Glasgow, Scotland. (22 pages)

Dan Craigen discusses the strengths and weaknesses of existing verification systems, presents a characterization of a "state-of-the-art" system, and discusses briefly some current research efforts.