jStar: towards practical verification for java

ABSTRACT

In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical developments in program verification: it combines the idea of abstract predicate families and the idea of symbolic execution and abstraction using separation logic. The proposed technology has been implemented in a new automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate the effectiveness of our methodology by using jStar to verify example programs implementing four popular design patterns (subject/observer, visitor, factory, and pooling). Although these patterns are extensively used by object-oriented developers in real-world applications, so far they have been highly challenging for existing object-oriented verification techniques.

REFERENCES

• 1: Anindya Banerjee , David A. Naumann , Stan Rosenberg, Regional Logic for Local Reasoning about Global Invariants, Proceedings of the 22nd European conference on Object-Oriented Programming, July 07-11, 2008, Paphos, Cypress [doi>10.1007/978-3-540-70592-5_17]
• 2: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec programming system: An overview. In Proceedings of CASSIS, pages 49--69, 2005.
• 3: M. Barnett and D. A. Naumann. Friends need a bit more: Maintaining invariants over shared state. In MPC, volume 3125 of LNCS, pages 54--84. Springer, 2004.
• 4: J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO 2005, volume 4111 of LNCS, pages 115--137. Springer, 2006.
• 5: J. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. In Proceedings of APLAS, volume 3780 of LNCS, pages 52--68. Springer, 2005.
• 6: L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. In Proceedings of FMICS, pages 73--89, 2003.
• 7: Wei-Ngan Chin , Cristina David , Huu Hai Nguyen , Shengchao Qin, Enhancing modular OO verification with separation logic, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 8: 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]
• 9: D. Distefano, P. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In Proceedings of TACAS, volume 3920 of LNCS, pages 287--302. Springer, 2006.
• 10: M. Dwyer, J.Hatcliff, M.Hoosier, and Robby. Building your own software model checker using the bogor extensible model checking framework. In CAV, volume 3576 of LNCS, pages 148--152. Springer, 2005.
• 11: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 12: M. Grand. Patterns in Java. Wiley, second edition, 2002.
• 13: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 14: I. T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In FM, volume 4085 of LNCS, pages 268--283. Springer, 2006.
• 15: N. R. Krishnaswami, J. Aldrich, and L. Birkedal. Modular verification of the subject-observer pattern via higher-order separation logic. In Proceedings of FTfJP, 2007.
• 16: Gary T. Leavens , K. Rustan M. Leino , Peter Müller, Specification and verification challenges for sequential object-oriented programs, Formal Aspects of Computing, v.19 n.2, p.159-189, June 2007 [doi>10.1007/s00165-007-0026-7]
• 17: Gary T. Leavens , Albert L. Baker , Clyde Ruby, Preliminary design of JML: a behavioral interface specification language for java, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006 [doi>10.1145/1127878.1127884]
• 18: K. R. M. Leino and W. Schulte. Using history invariants to verify observers. In Proceedings of ESOP, volume 4421 of LNCS, pages 80--94. Springer, 2007.
• 19: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 20: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 21: Peter Müller , Arnd Poetzsch-Heffter , Gary T. Leavens, Modular invariants for layered object structures, Science of Computer Programming, v.62 n.3, p.253-286, 15 October 2006 [doi>10.1016/j.scico.2006.03.001]
• 22: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 23: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 24: M. J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.
• 25: Matthew Parkinson , Gavin Bierman, Separation logic and abstraction, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.247-258, January 12-14, 2005, Long Beach, California, USA
• 26: Matthew J. Parkinson , Gavin M. Bierman, Separation logic, abstraction and inheritance, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 27: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 28: J. Smans, B. Jacobs, F. Piessens, and W. Schulte. An automatic verifier for java-like programs based on dynamic frames. In Proceedings of FASE, volume 4961 of LNCS, pages 261--275. Springer, 2008.
• 29: R. Vallée-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot -- a java optimization framework. In Proceedings of CASCON 1999, pages 125--135, 1999.
• 30: Xianghua Deng , Jooyong Lee , Robby, Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.157-166, September 18-22, 2006 [doi>10.1109/ASE.2006.26]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Inheritance

General Terms:
Languages, Theory, Verification

Keywords:
classes, design patterns, moduarity, separation logic