This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ADI: Automatic Derivation of Invariants
January 1980 (vol. 6 no. 1)
pp. 40-48
M. Tamir, Department of Applied Mathematics, Weizmann Institute of Science
Most current systems for mechanical program verification are not fully automatic, since the user himself must provide the intermediate inductive assertions. This paper describes an interactive computer program, called ADI, which automatically generates the needed inductive assertions. ADI is also able to extend partial loop assertions supplied by the user to form complete assertions. The implementation (written in QLISP and INTERLISP) is based on both the algorithmic and the heuristic approaches introduced by Katz and Manna in "Logical Analysis of Programs" [25]. For the algorithmic subsystem ADI includes: Difference Equations Constructor, Difference Equations Solver, and Invariants from Conditional Statements Generator. The heuristic subsystem includes: Exit Rules Package, Bounding Variables Component, Strengthening Executer, Weakening Executer, and a Heuristic Invariant Matcher-which is the actual implementation of two new heuristics, MATCHPQ and MATCHPT. ADI is a small step toward interactive, practical program verification.
Index Terms:
synthesis of invariants, Assertions, invariants, partial correctness, program verification, QLISP
Citation:
M. Tamir, "ADI: Automatic Derivation of Invariants," IEEE Transactions on Software Engineering, vol. 6, no. 1, pp. 40-48, Jan. 1980, doi:10.1109/TSE.1980.230461
Usage of this product signifies your acceptance of the Terms of Use.