Reachability analysis for annotated code

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Reachability analysis for annotated code

Full text

Pdf (521 KB)

Source

Foundations of Software Engineering archive
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 table of contents

Dubrovnik, Croatia

Pages: 23 - 30

Year of Publication: 2007

ISBN:978-1-59593-721-6

Authors

Mikoláš Janota	University College Dublin, Belfield, Dublin, Ireland
Radu Grigore	University College Dublin, Belfield, Dublin, Ireland
Michal Moskal	University of Wroclaw, Wroclaw, Poland

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 34, Citation Count: 1

Additional Information:

abstract references cited by 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/1292316.1292319 What is a DOI?

ABSTRACT

Well-specified programs enable code reuse and therefore techniques that help programmers to annotate code correctly are valuable. We devised an automated analysis that detects unreachable code in the presence of code annotations. We implemented it as an enhancement of the extended static checker ESC/Java2 where it serves as a check of coherency of specifications and code. In this article we define the notion of semantic unreachability, describe an algorithm for checking it and demonstrate on a case study that it detects a class of errors previously undetected, as well as describe different scenarios of these errors.

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	Parosh Aziz Abdulla , Per Bjesse , Niklas Eén, Symbolic Reachability Analysis Based on SAT-Solvers, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.411-425, March 25-April 02, 2000
	2	M. Barnett, K. Leino, and W. Schulte. The Spec# programming system: An overview. In Proceeding of CASSIS 2004, volume 3362 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
	3	Jan Olaf Blech , Lars Gesellensetter , Sabine Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.200-209, September 07-09, 2005 [doi>10.1109/SEFM.2005.20]
	4	F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. Symbolic animation of JML specifications. In Proceedings of Formal Methods, International Symposium of Formal Methods (FM 2005), Lecture Notes in Computer Science. Springer-Verlag, 2005.
	5	Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
	6	Patrice Chalin, Early detection of JML specification errors using ESC/Java2, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181201]
	7	S. Chatterjee, S. Lahiri, S. Qadeer, and Z. Rakamaric. A reachability predicate for analyzing low-level software. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
	8	K. D. Cooper, T. J. Harvey, and K. Kennedy. A simple, fast dominance algorithm, 2001. Available online at www.cs.rice.edu/~keith/EMBED/dom.pdf.
	9	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]
	10	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]
	11	R. DeLine and K. R. M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical report, Microsoft Research, 2005.
	12	David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
	13	Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
	14	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
	15	L. Friendly. The design of distributed hyperlinked programming documentation. IWHD, 95:151--173, 1995.
	16	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	17	M. Janota. Assertion-based loop invariant generation. In Proceedings of the 1st International Workshop on Invariant Generation (WING '07), June 2007.
	18	J. R. Kiniry and D. R. Cok. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004, volume 3362 of Lecture Notes in Computer Science. Springer-Verlag, Jan. 2005.
	19	Donald E. Knuth, Literate programming, The Computer Journal, v.27 n.2, p.97-111, May 1984 [doi>10.1093/comjnl/27.2.97]
	20	Charles W. Krueger, Software reuse, ACM Computing Surveys (CSUR), v.24 n.2, p.131-183, June 1992 [doi>10.1145/130844.130856]
	21	Haim Kilov , Bernhard Rumpe , Ian D. Simmonds, Behavioral Specifications of Businesses and Systems, Kluwer Academic Publishers, Norwell, MA, 1999
	22	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]
	23	K. R. M. Leino and F. Logozzo. Loop invariants on demand. In Proceedings of The Third Asian Symposium on Programming Languages and Systems (APLAS 2005), volume 3780 of Lecture Notes in Computer Science. Springer-Verlag, 2005.
	24	K. Rustan M. Leino , Todd Millstein , James B. Saxe, Generating error traces from verification-condition counterexamples, Science of Computer Programming, v.55 n.1-3, p.209-226, March 2005 [doi>10.1016/j.scico.2004.05.016]
	25	K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. Technical Note 1999--002, Compaq SRC, May 1999.
	26	Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
	27	Jacobo Valdes , Robert E. Tarjan , Eugene L. Lawler, The recognition of Series Parallel digraphs, Proceedings of the eleventh annual ACM symposium on Theory of computing, p.1-12, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804393]