Specification and verification challenges for sequential object-oriented programs
				  by
	Gary T. Leavens, K. Rustan M. Leino, and Peter Mueller

			       Abstract

The state of knowledge in how to specify sequential programs in
object-oriented languages such as Java and C# and the state of the
art in automated verification tools for such programs have made
measurable progress in the last several years.  This paper describes
several remaining challenges and approaches to their solution.


Keywords: Program verification, specification, contract,
object-oriented programming, challenge, JML, Spec#.

2000 CR Categories:
D.2.4 [Software Engineering] Software/Program Verification
       --- Formal methods, programming by contract, reliability, tools,
	   JML;
F.3.1 [Logics and Meanings of Programs]
       Specifying and Verifying and Reasoning about Programs ---
        Assertions, pre- and post-conditions,
        specification techniques;

Submitted for publication.

Copyright (c) 2006 by Gary T. Leavens, K. Rustan M. Leino, and Peter Mueller.
All rights reserved.