Title :
What Can We Expect from Program Verification?
Author :
Jackson, Michael
Author_Institution :
Dept. of Comput., Open Univ., Milton Keynes
Abstract :
Program verification assumes a formal program specification. In software-intensive systems, such specifications must depend on formalization of the natural, nonformal problem world. This formalization is inevitably imperfect, and poses major difficulties of structure and reasoning. Appropriate verification tools can help address these difficulties and improve system reliability
Keywords :
formal specification; program verification; software reliability; software tools; formal program specification; program verification tools; software-intensive system reliability; Computer interfaces; Formal specifications; Humans; Maintenance engineering; Mathematics; Roads; Software maintenance; Telephony; Terminology; Tides; program verification; software engineering; software-intensive systems; system reliability;
DOI :
10.1109/MC.2006.363