Title: An industrial-strength method for the construction of formally verified software
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.
Publication Year: 2002
Publication Date: 2002-12-23
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 6
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot