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