research-article

ESC4: a modern caching ESC for Java

Authors:

Perry R. James,

Patrice ChalinAuthors Info & Claims

SAVCBS '09: Proceedings of the 8th international workshop on Specification and verification of component-based systems

Pages 19 - 26

https://doi.org/10.1145/1596486.1596491

Published: 25 August 2009 Publication History

Get Access

Abstract

JML4 is an Eclipse-based Integrated Verification Environment for the Java Modeling Language (JML) that supports several forms of verification, including Runtime Assertion Checking, Extended Static Checking (ESC), and Full Static Program Verification. The first of these developed was ESC4, JML4's ESC component. This paper presents its architecture. ESC4's verification-condition (VC) generation is based on the approach described by Barnett and Leino, but we provide an optimization for loops. A configurable Prover Coordinator allows the easy implementation of various proof strategies. Caching discharged VCs helps reduce the number of calls to the provers when reverifying code. Caches are not commonly used because of their fragility w.r.t. source code changes, but we propose a simple way to make them more resilient.

References

[1]

BARNETT, M., AND LEINO, K. R. M. Weakest-precondition of unstructured programs. In PASTE '05: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (New York, NY, 2005), ACM Press, pp. 82--87.

Digital Library

Google Scholar

[2]

COK, D. R., AND KINIRY, J. R. ESC/Java2: Uniting ESC/Java and JML. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (2005), vol. 3362/2005 of LNCS, Springer Berlin, pp. 108--128.

Digital Library

Google Scholar

[3]

CORMEN, T. H., LEISERSON, C. E., AND RIVEST, R. L. Introduction to Algorithms. The MIT Press, Cambridge, MA, 1990.

Digital Library

Google Scholar

[4]

DIJKSTRA, E. W. A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs, NJ, 1976.

Digital Library

Google Scholar

[5]

GAMMA, E., HELM, R., JOHNSON, R., AND VLISSIDES, J. Design patterns: elements of reusable object-oriented software. Addison-Wesley Professional, Boston, MA, 1995.

Digital Library

Google Scholar

[6]

JAMES, P. R., AND CHALIN, P. Enhanced extended static checking in JML4: Benefits of multiple-prover support. In ACM SAC 2009 (24th Annual ACM Symposium on Applied Computing) (2009).

Digital Library

Google Scholar

[7]

JAMES, P. R., AND CHALIN, P. Faster and more complete extended static checking for the java modeling language. Journal of Automated Reasoning (2009). to appear.

Digital Library

Google Scholar

[8]

JAMES, P. R., CHALIN, P., GIANNAS, L., AND KARABOTSOS, G. Distributed, multi-threaded verification of Java programs. In SAVCBS '08: Proceedings of the 2008 workshop on Specification and verification of component-based systems (2008).

Google Scholar

[9]

LEINO, K. R. M., STATA, R., SAXE, J. B., AND FLANAGAN, C. Java to guarded commands translation. Technical Report ESCJ 16c, Compaq, 1998. Available from the ESC/Java2 website.

Google Scholar

Cited By

View all

Brain MSchanda F(2012)A lightweight technique for distributed and incremental program verificationProceedings of the 4th international conference on Verified Software: theories, tools, experiments10.1007/978-3-642-27705-4_10(114-129)Online publication date: 28-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27705-4_10

Index Terms

ESC4: a modern caching ESC for Java

Recommendations

Faster and More Complete Extended Static Checking for the Java Modeling Language

Extended Static Checking (ESC) is a fully automated formal verification technique. Verification in ESC is achieved by translating programs and their specifications into verification conditions (VCs). Proof of a VC establishes the correctness of the ...
Extended static checking in JML4: benefits of multiple-prover support
SAC '09: Proceedings of the 2009 ACM symposium on Applied Computing

The implementations of many seemingly simple algorithms are beyond the ability of traditional Extended Static Checking (ESC) tools to verify. Not being able to verify toy examples is often enough to turn users off of the idea of using formal methods. ...
An integrated verification environment for JML: architecture and early results
SAVCBS '07: Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering

Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively high: e.g., almost three years following its release, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SAVCBS '09: Proceedings of the 8th international workshop on Specification and verification of component-based systems

August 2009

42 pages

ISBN:9781605586809

DOI:10.1145/1596486

Program Chair:
Marieke Huisman
University of Twente, Netherlands

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESEC/FSE09

Sponsor:

ESEC/FSE09: Joint 12th European Software Engineering Conference

August 25, 2009

Amsterdam, The Netherlands

Acceptance Rates

Overall Acceptance Rate 37 of 46 submissions, 80%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
110
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Brain MSchanda F(2012)A lightweight technique for distributed and incremental program verificationProceedings of the 4th international conference on Verified Software: theories, tools, experiments10.1007/978-3-642-27705-4_10(114-129)Online publication date: 28-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27705-4_10

View Options

Get Access

Login options

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

Cited By

Index Terms

Recommendations

Faster and More Complete Extended Static Checking for the Java Modeling Language

Extended static checking in JML4: benefits of multiple-prover support

An integrated verification environment for JML: architecture and early results