Roadmap for Enhanced Languages and Methods to Aid Verification

Leavens, G. T., Abrial, J. R., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C. B., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D. R. and Stump, A. (2006) Roadmap for Enhanced Languages and Methods to Aid Verification. In Proceedings of Generative Programming and Component Engineering, 5th International, Portland, Oregon.

---

Downloads

PDF - Requires Adobe Acrobat Reader or other PDF viewer.

340Kb

Abstract

This roadmap describes ways that researchers in four areas — speci-
fication 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.

• Item Type Conference or Workshop Item
• Additional Information A VSTTE committee roadmap. 146 references.
• Research Group Dependable Systems and Software Engineering Research Group
• Deposited On 10 August 2006 by Butler, Michael
• Alternative Locations ftp://ftp.cs.iastate.edu/pub/techreports/TR06-21/TR.pdf
• ID Code 12885
• Performance Indicator EZ~13~01~04

Authors

• Gary T. Leavens
• Jean-Raymond Abrial
• Don Batory
• Michael Butler
• Alessandro Coglio
• Kathi Fisler
• Eric Hehner
• Cliff B. Jones
• Dale Miller
• Simon Peyton-Jones
• Murali Sitaraman
• Douglas R. Smith
• Aaron Stump

Corrections

ECS staff and postgraduates may modify this record.

Tagging

Download Statistics

Members of ECS may view the download statistics dashboard for this record.

Metadata

Metadata available via OAI as: oai_dc (unqualified dublin core)