Predicate abstraction for software verification

ABSTRACT

Software verification is an important and difficult problem. Many static checking techniques for software require annotations from the programmer in the form of method specifications and loop invariants. This annotation overhead, particularly of loop invariants, is a significant hurdle in the acceptance of static checking. We reduce the annotation burden by inferring loop invariants automatically.Our method is based on predicate abstraction, an abstract interpretation technique in which the abstract domain is constructed from a given set of predicates over program variables. A novel feature of our approach is that it infers universally-quantified loop invariants, which are crucial for verifying programs that manipulate unbounded data such as arrays. We present heuristics for generating appropriate predicates for each loop automatically; the programmer can specify additional predicates as well. We also present an efficient algorithm for computing the abstraction of a set of states in terms of a collection of predicates.Experiments on a 44KLOC program show that our approach can automatically infer the necessary predicates and invariants for all but 31 of the 396 routines that contain loops.

REFERENCES

• BBM97: Nikolaj Bjørner , Anca Browne , Zohar Manna, Automatic generation of invariants and intermediate assertions, Theoretical Computer Science, v.173 n.1, p.49-87, Feb. 1997 [doi>10.1016/S0304-3975(96)00191-0]
• BLS96: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• BMMR01: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• Bry86: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• BvW98: Ralph-Johan J. Back , Abo Akademi , J. Von Wright , F. B. Schneider , D. Gries, Refinement Calculus: A Systematic Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• CC77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• CGJ+00: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• CH78: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• DDP99: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• Dij76: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• DLNS98: D.L.Detlefs,K.R.M.Leino,C.G.Nelson,and J.B. Saxe.Extended static checking.Research Report 159,Compaq Systems Research Center,December 1998.
• FS01: Cormac Flanagan , James B. Saxe, Avoiding exponential explosion: generating compact verification conditions, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.193-205, January 2001, London, United Kingdom
• GS97: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• GW74: Irene Greif , Richard J. Waldinger, A more mechanical approach to program verification, Programming Symposium, Proceedings Colloque sur la Programmation, p.109-119, April 09-11, 1974
• GW75: S.M.German and B.Wegbreit.A synthesizer of inductive assertions.IEEE Transactions on Software Engineering SE-1(1):68 -75,1975.
• KM76: Shmuel Katz , Zohar Manna, Logical analysis of programs, Communications of the ACM, v.19 n.4, p.188-206, April 1976 [doi>10.1145/360032.360048]
• LSS99: K.R.M.Leino,J.B.Saxe,and R.Stata.Checkin Java programs via guarded commands.In Bart Jacobs,Gary T.Leavens,Peter Muller,and Arnd Poetzsch-Heffter,editors,Formal Techniques for Java Programs Technical Report 251.Fernuniversitat Hagen,May 1999.
• MP92: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• Nel81: C.G.Nelson.Techniques for program verification. Technical Report CSL-81-10,Xerox Palo Alto Research Center,1981.
• Nel89: Greg Nelson, A generalization of Dijkstra's calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.517-561, Oct. 1989 [doi>10.1145/69558.69559]
• SI77: Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512963]
• SS99: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• TML97: Chandramohan A. Thekkath , Timothy Mann , Edward K. Lee, Frangipani: a scalable distributed file system, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.224-237, October 05-08, 1997, Saint Malo, France
• Weg74: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]