archives

Specification and verification challenges for sequential object-oriented programs


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T., Leino, K. Rustan M. and Müller, Peter (2006) Specification and verification challenges for sequential object-oriented programs. Technical Report TR#06-14, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

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.

Keywords:Program verification, specification, contract, object-oriented programming, challenge, JML, Spec#.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000422
Deposited by:Gary T. Leavens on 17 May 2006
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR06-14/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-14/TR.ps.gz

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu