Lessons from the JML Project
|
Home About Browse Search Register Subscriptions Deposit Papers Help |
Leavens, Gary T. and Clifton, Curtis (2005) Lessons from the JML Project. Technical Report 05-12a, Computer Science, Iowa State University.
| Full text available as: | Adobe PDF Postscript |
This is the latest version of this eprint.
Abstract
To have impact, a grand challenge should provide a way for diverse research to be integrated in a synergistic fashion. Synergy in the JML project comes from a shared specification language, and thus holds several lessons for the verifying compiler grand challenge. An important lesson is that the project should focus considerable resources on specification language design, which still contains many open research problems. Another important lesson is that, to support such a specification language, the project needs to involve groups doing research on extensible compilers and integrated development environments.
| Keywords: | verifying compiler, specification, verification, formal methods, formal interface specification, extensible compilers, integrated development environments, JML language, Java language, Hoare. |
| Subjects: | Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1) Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1) Software: SOFTWARE ENGINEERING (K.6.3): Programming Environments 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: | 00000376 |
| Deposited by: | Gary T. Leavens on 22 July 2005 |
| Alternative Locations: | ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.ps.gz |
Available Versions of This Paper
- Lessons from the JML Project (deposited 05 May 2005)
- Lessons from the JML Project (deposited 22 July 2005) [Currently displayed]
Contact site administrator at: ssg@cs.iastate.edu