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 06-14, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

This is the latest version of this eprint.

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#.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.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:00000455
Deposited by:Gary T. Leavens on 11 September 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