INVESTIGATION OF RUN-TIME ISSUES IN VERIFIED SOFTWARE
- Authors
- 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
Document 1 of 1
- Date modified: