Extended static checking in JML4

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

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

Full text

Pdf (356 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2009 ACM symposium on Applied Computing table of contents

Honolulu, Hawaii

SESSION: Software verification and testing track table of contents

Pages 609-614

Year of Publication: 2009

ISBN:978-1-60558-166-8

Authors

Perry R. James	Concordia University, Montreal, Canada
Patrice Chalin	Concordia University, Montreal, Canada

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 31, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1529282.1529410 What is a DOI?

ABSTRACT

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. ESC4, the ESC component of the JML4 project, is able to verify many more kinds of methods in part because of its use of novel techniques which apply multiple theorem provers. In particular, we present Offline User-Assisted ESC (OUA-ESC), a new form of verification that lies between ESC and Full Static Program Verification (FSPV), that allows users to control the level of completeness of the tool. ESC4's improved performance should encourage greater use of static verification.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Isabelle, 2008. Homepage at http://isabelle.in.tum.de.
	2	Metis theorem prover, 2008. Homepage at http://www.gilith.com/software/metis/.
	3	Proof General Eclipse, 2008. Homepage at http://proofgeneral.inf.ed.ac.uk/eclipse.
	4	Why: software verification platform, 2008. Homepage at http://why.lri.fr.
	5	Mike Barnett , K. Rustan M. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
	6	Barnett, M., Leino, K. R. M., and Schulte, W. The Spec# Programming System: An overview. In CASSIS 2004: International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (2004), pp. 49--69.
	7	Sascha Böhme , K. Rustan Leino , Burkhart Wolff, HOL-Boogie -- An Interactive Prover for the Boogie Program-Verifier, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, August 18-21, 2008, Montreal, P.Q., Canada [doi>10.1007/978-3-540-71067-7_15]
	8	Patrice Chalin , Perry R. James , George Karabotsos, An integrated verification environment for JML: architecture and early results, 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, p.47-53, September 03-04, 2007, Dubrovnik, Croatia [doi>10.1145/1292316.1292322]
	9	Patrice Chalin , Perry R. James , George Karabotsos, JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML, Proceedings of the 2nd international conference on Verified Software: Theories, Tools, Experiments, October 06-09, 2008, Toronto, Canada [doi>10.1007/978-3-540-87873-5_9]
	10	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.
	11	Filliâtre, J.-C. The WHY verification tool: Tutorial and reference manual, 2008. Available at http://why.lri.fr.
	12	Filliâtre, J.-C., Hubert, T., and Marché, C. The Caduceus verification tool for C programs: Tutorial and reference manual, 2008. Available at http://caduceus.lri.fr.
	13	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	14	Karabotsos, G., Chalin, P., James, P. R., and Giannas, L. Total correctness of recursive functions using JML4FSPV. In SAVCBS '08: Proceedings of the 2008 Workshop on Specification and Verification of Component-Based Systems (2008).
	15	B Kolman , R C Busby, Discrete mathematical structures for computer science (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	16	Leavens, G. T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., and Chalin, P. JML reference manual, 2008. Available at http://www.jmlspecs.org.
	17	Leino, K. R. M., and Monahan, R. Automatic verification of textbook programs that use comprehensions. In FTfJP '07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (2007).
	18	Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
	19	Paulson, L. C., and Susanto, K. W. Source-level proof reconstruction for interactive theorem proving. In Theorem Proving in Higher Order Logics: TPHOLs 2007 (2007), K. Schneider and J. Brandt, Eds., LNCS 4732, Springer, pp. 232--245.
	20	Markus Wenzel, Isar - A Generic Interpretative Approach to Readable Formal Proof Documents, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.167-184, September 01, 1999