INVESTIGATION OF RUN-TIME ISSUES IN VERIFIED SOFTWARE

Authors
  1. Laferriere, C.
Corporate Authors
Intellitech Canada Ltd, Ottawa ONT (CAN);Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
Abstract
The purpose of this report is to examine the issues connected with the verifiability of concurrent programs and of programs dealing with low-level devices. This investigation is to take place in the context of m-Verdi/m-EVES. m-Verdi is a programming language with a sound mathematical foundation which is used to write software that will be subsequently verified. m-EVES is the verification environment which is used to verify programs written in m-Verdi. m-EVES is composed of a Verification Condition Generator, a Theorem Prover, and other utilities. One of the characteristics of the m-Verdi/m-EVES combination is that it does not cater to concurrency. This project intends to look at what can be achieved in terms of proofs of corrections when m-Verdi/m-EVES is confronted with concurrent systems.
Report Number
INT-87-72 —
Date of publication
15 Dec 1987
Number of Pages
15
DSTKIM No
90-04513
CANDIS No
66746
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: