research-article

jStar: towards practical verification for java

Authors:

Dino Distefano,

Matthew J. Parkinson JAuthors Info & Claims

OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications

Pages 213 - 226

https://doi.org/10.1145/1449764.1449782

Published: 19 October 2008 Publication History

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]

A. Banerjee, D. Naumann, and S. Rosenberg. Regional logic for local reasoning about global invariants. In Proceeding of ECOOP, volume 5142 of LNCS, pages 387--411. Springer, 2008.

[2]

M. Barnett, K. R. M. Leino, and W. Schulte. The Spec programming system: An overview. In Proceedings of CASSIS, pages 49--69, 2005.

Digital Library

[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.

Digital Library

[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]

W.-N. Chin, C. David, H. Nguyen, and S. Qin. Enhancing modular OO verification with separation logic. In Proceedings of POPL, pages 87--99. ACM, 2008.

Digital Library

[8]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL '77: Principles of Programming Languages, pages 238--252. ACM Press, 1977.

Digital Library

[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]

E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, 1994.

Digital Library

[12]

M. Grand. Patterns in Java. Wiley, second edition, 2002.

[13]

S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In 28th POPL 2001, pages 14--26, 2001.

Digital Library

[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]

G. Leavens, K. Leino, and P.Müller. Specification and verification challenges for sequential object--oriented programs. Formal Aspects of Computing, 19(2):159--189, 2007.

[17]

G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Software Engineering Notes, 31(3):1--38, 2006.

Digital Library

[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.

Digital Library

[19]

T. Lev-Ami and M. Sagiv. Tvla: A system for implementing static analyses. In SAS, volume 1824 of LNCS, pages 280--301. Springer, 2000.

Digital Library

[20]

B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM TOPLAS, 16(6):1811--1841, 1994.

Digital Library

[21]

P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular invariants for layered object structures. Science of Computer Programming, 62:253--286, 2006.

Digital Library

[22]

P. W. O'Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Proceedings of CSL, volume 2142 of LNCS, pages 1--19. Springer, 2001.

Digital Library

[23]

P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In 31st POPL 2004, pages 268--280, 2004.

Digital Library

[24]

M. J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.

[25]

M. J. Parkinson and G. M. Bierman. Separation logic and abstraction. In 32nd POPL 2005, pages 247--258, 2005.

Digital Library

[26]

M. J. Parkinson and G. M. Bierman. Separation logic, abstraction and inheritance. In Proceedings of POPL, pages 75--86. ACM, 2008.

Digital Library

[27]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape--analysis problems in languages with destructive updating. ACM TOPLAS, 20(1):1--50, 1998.

Digital Library

[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.

Digital Library

[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]

X.Deng, J.Lee, and Robby. Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In ASE 2006, pages 157--166. IEEE, 2006.

Digital Library

Cited By

de Boer Fde Gouw SHiep HBian J(2025)Footprint Logic for Object-Oriented Components (extended paper)Formal Aspects of Computing10.1145/370392137:2(1-23)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3703921
DiVincenzo JMcCormack IZimmerman CGouni HGorenburg JRamos-Dávila JZhang MSunshine JTanter ÉAldrich J(2024)Gradual C0: Symbolic Execution for Gradual VerificationACM Transactions on Programming Languages and Systems10.1145/370480846:4(1-57)Online publication date: 5-Dec-2024
https://dl.acm.org/doi/10.1145/3704808
Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://doi.org/10.1145/3656450
Show More Cited By

Recommendations

jStar: towards practical verification for java

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 ...
jStar-eclipse: an IDE for automated verification of Java programs
ESEC/FSE '11: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering

jStar is a tool for automatically verifying Java programs. It uses separation logic to support abstract reasoning about object specifications. jStar can verify a number of challenging design patterns, including Subject/Observer, Visitor, Factory and ...
Separation logic, abstraction and inheritance
POPL '08

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications

October 2008

654 pages

ISBN:9781605582153

DOI:10.1145/1449764

General Chair:
Gail E. Harris
Instantiated Software Inc.
,
Program Chairs:
Gregor Kiczales
University of British Columbia
,
Dirk Riehle
SAP Research
,
Andrew P. Black
Portland State University

ACM SIGPLAN Notices Volume 43, Issue 10
September 2008
613 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1449955
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

OOPSLA08

Sponsor:

OOPSLA08: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

October 19 - 23, 2008

TN, Nashville, USA

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

206
Total Citations
View Citations
815
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)3

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

de Boer Fde Gouw SHiep HBian J(2025)Footprint Logic for Object-Oriented Components (extended paper)Formal Aspects of Computing10.1145/370392137:2(1-23)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3703921
DiVincenzo JMcCormack IZimmerman CGouni HGorenburg JRamos-Dávila JZhang MSunshine JTanter ÉAldrich J(2024)Gradual C0: Symbolic Execution for Gradual VerificationACM Transactions on Programming Languages and Systems10.1145/370480846:4(1-57)Online publication date: 5-Dec-2024
https://dl.acm.org/doi/10.1145/3704808
Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://doi.org/10.1145/3656450
Bian JHiep Hde Boer Fde Gouw S(2023)Integrating ADTs in KeY and their application to history-based reasoning about collectionFormal Methods in System Design10.1007/s10703-023-00426-x61:1(63-89)Online publication date: 9-May-2023
https://doi.org/10.1007/s10703-023-00426-x
Uhlig FXu A(2023)Iterative optimal solutions of linear matrix equations for hyperspectral and multispectral image fusingCalcolo: a quarterly on numerical analysis and theory of computation10.1007/s10092-023-00514-860:2Online publication date: 27-Apr-2023
https://dl.acm.org/doi/10.1007/s10092-023-00514-8
Keuchel SHuyghebaert SLukyanov GDevriese D(2022)Verified symbolic execution with Kripke specification monads (and no meta-programming)Proceedings of the ACM on Programming Languages10.1145/35476286:ICFP(194-224)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547628
de Boer Fde Gouw SHiep HBian J(2022)Footprint Logic for Object-Oriented ComponentsFormal Aspects of Component Software10.1007/978-3-031-20872-0_9(141-160)Online publication date: 2-Nov-2022
https://doi.org/10.1007/978-3-031-20872-0_9
Bian JHiep Hde Boer Fde Gouw S(2021)Integrating ADTs in KeY and Their Application to History-Based ReasoningFormal Methods10.1007/978-3-030-90870-6_14(255-272)Online publication date: 10-Nov-2021
https://doi.org/10.1007/978-3-030-90870-6_14
Rubbens RLathouwers SHuisman M(2021)Modular Transformation of Java Exceptions Modulo ErrorsFormal Methods for Industrial Critical Systems10.1007/978-3-030-85248-1_5(67-84)Online publication date: 19-Aug-2021
https://doi.org/10.1007/978-3-030-85248-1_5
Maksimović PAyoun SSantos JGardner P(2021)Gillian, Part II: Real-World Verification for JavaScript and CComputer Aided Verification10.1007/978-3-030-81688-9_38(827-850)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_38
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten