An industrial-strength method for the construction of formally verified software

Author

Lindsay, Peter ; Hemer, David

Author_Institution

Dept. of Comput. Sci., Queensland Univ., St. Lucia, Qld., Australia

fYear

1996

fDate

14-18 Jul 1996

Firstpage

27

Lastpage

36

Abstract

The CARE method is a new approach to constructing and formally verifying programs. CARE has been developed in response to identified industrial needs for a formal software development method which does not require the user to be an expert in formal proof. Software engineers use CARE to develop compilable code from formal program specifications using a library of pre-proven, formally specified refinements. Tools help users build products by selecting and instantiating refinements to fit the problem at hand, and generating and discharging correctness-of-fit proof obligations. The paper introduces CARE´s integrated notation for algorithm specification and development, and explains how correctness is checked. The method is illustrated on a small development

Keywords

formal specification; program verification; programming theory; CARE method; algorithm specification; compilable code; correctness-of-fit proof obligations; formal program specifications; formal proof; formal software development method; formally specified refinements; formally verified software; industrial needs; industrial strength method; Collaborative software; Computer industry; Computer science; Computer security; Construction industry; Formal specifications; Libraries; National security; Programming; Refining;

fLanguage

English

Publisher

ieee

Conference_Titel

Australian Software Engineering Conference, 1996., Proceedings of 1996

Conference_Location

Melbourne, Vic.

Print_ISBN

0-8186-7635-3

Type

conf

DOI

10.1109/ASWEC.1996.534120

Filename

534120