Access Restriction

Author Wegbreit, Ben
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Weak interpretations ♦ Inductive assertions ♦ Loop predicates ♦ Theorem proving ♦ Property extraction ♦ Synthesis of loop predicates ♦ Well-founded sets ♦ Program verification
Abstract Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error prone, producing a program with complete, correct predicates is reasonably difficult and would be facilitated by machine assistance. This paper discusses techniques for mechanically synthesizing loop predicates. Two classes of techniques are considered: (1) heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions: (2) extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicates by an evaluation on the weak interpretation.
Description Affiliation: Harvard Univ., and Xerox Palo Alto Research Center, Palo Alto, CA (Wegbreit, Ben)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 17
Issue Number 2
Page Count 12
Starting Page 102
Ending Page 113

Open content in new tab

   Open content in new tab
Source: ACM Digital Library