archives

Roadmap for Enhanced Languages and Methods to Aid Verification


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, Hehner, Eric, Jones, Cliff, Miller, Dale, Peyton-Jones, Simon, Sitaraman, Murali, Smith, Douglas R. and Stump, Aaron (2006) Roadmap for Enhanced Languages and Methods to Aid Verification. Technical Report 06-21, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

Abstract

This roadmap describes ways that researchers in four areas -- specification languages, program generation, correctness by construction, and programming languages -- might help further the goal of verified software. It also describes what advances the ``verified software'' grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas. A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Keywords:Verification, verified software grand challenge, specification languages, program generation, correctness by construction, programming languages, tools, annotations.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Programming Environments
Software: SOFTWARE ENGINEERING (K.6.3): Distribution, Maintenance, and Enhancement
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Classifications
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
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)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
Computer Applications: COMPUTERS IN OTHER SYSTEMS (C.3)
ID code:00000438
Deposited by:Gary T. Leavens on 21 July 2006
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR06-21/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-21/TR.ps.gz



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