Roadmap for enhanced languages and methods to aid verification

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

doi:10.1145/1173706.1173740

Roadmap for enhanced languages and methods to aid verification

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006
Publisher	Association for Computing Machinery (ACM)
Pages	221-236
Number of pages	16
ISBN (Print)	1595932372, 9781595932372
DOIs	https://doi.org/10.1145/1173706.1173740
Publication status	Published - 1 Jan 2006
Externally published	Yes
Event	5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006 - Portland, OR, United States Duration: 22 Oct 2006 → 26 Oct 2006

Publication series

Name	Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06

Conference

Conference	5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006
Country/Territory	United States
City	Portland, OR
Period	22/10/06 → 26/10/06

Keywords

Annotations
Correctness by construction
Program generation
Programming languages
Specification languages
Tools
Verification
Verified software grand challenge

Access to Document

10.1145/1173706.1173740

Cite this

Leavens, G. T., Abrial, J. R., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D. R., & Stump, A. (2006). Roadmap for enhanced languages and methods to aid verification. In Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006 (pp. 221-236). (Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06). Association for Computing Machinery (ACM). https://doi.org/10.1145/1173706.1173740

Leavens, Gary T. ; Abrial, Jean Raymond ; Batory, Don et al. / Roadmap for enhanced languages and methods to aid verification. Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006. Association for Computing Machinery (ACM), 2006. pp. 221-236 (Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06).

@inproceedings{8f2a9ac020534519babb4068d1d6edab,

title = "Roadmap for enhanced languages and methods to aid verification",

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 = "Annotations, Correctness by construction, Program generation, Programming languages, Specification languages, Tools, Verification, Verified software grand challenge",

author = "Leavens, \{Gary T.\} and Abrial, \{Jean Raymond\} and Don Batory and Michael Butler and Alessandro Coglio and Kathi Fisler and Eric Hehner and Cliff Jones and Dale Miller and Simon Peyton-Jones and Murali Sitaraman and Smith, \{Douglas R.\} and Aaron Stump",

year = "2006",

month = jan,

day = "1",

doi = "10.1145/1173706.1173740",

language = "English",

isbn = "1595932372",

series = "Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06",

publisher = "Association for Computing Machinery (ACM)",

pages = "221--236",

booktitle = "Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006",

note = "5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006 ; Conference date: 22-10-2006 Through 26-10-2006",

}

Leavens, GT, Abrial, JR, Batory, D, Butler, M, Coglio, A, Fisler, K, Hehner, E, Jones, C, Miller, D, Peyton-Jones, S, Sitaraman, M, Smith, DR & Stump, A 2006, Roadmap for enhanced languages and methods to aid verification. in Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006. Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06, Association for Computing Machinery (ACM), pp. 221-236, 5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, Portland, OR, United States, 22/10/06. https://doi.org/10.1145/1173706.1173740

Roadmap for enhanced languages and methods to aid verification. / Leavens, Gary T.; Abrial, Jean Raymond; Batory, Don et al.
Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006. Association for Computing Machinery (ACM), 2006. p. 221-236 (Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Roadmap for enhanced languages and methods to aid verification

AU - Leavens, Gary T.

AU - Abrial, Jean Raymond

AU - Batory, Don

AU - Butler, Michael

AU - Coglio, Alessandro

AU - Fisler, Kathi

AU - Hehner, Eric

AU - Jones, Cliff

AU - Miller, Dale

AU - Peyton-Jones, Simon

AU - Sitaraman, Murali

AU - Smith, Douglas R.

AU - Stump, Aaron

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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.

AB - 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.

KW - Annotations

KW - Correctness by construction

KW - Program generation

KW - Programming languages

KW - Specification languages

KW - Tools

KW - Verification

KW - Verified software grand challenge

U2 - 10.1145/1173706.1173740

DO - 10.1145/1173706.1173740

M3 - Conference contribution

AN - SCOPUS:34547459543

SN - 1595932372

SN - 9781595932372

T3 - Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06

SP - 221

EP - 236

BT - Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006

PB - Association for Computing Machinery (ACM)

T2 - 5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006

Y2 - 22 October 2006 through 26 October 2006

ER -

Leavens GT, Abrial JR, Batory D, Butler M, Coglio A, Fisler K et al. Roadmap for enhanced languages and methods to aid verification. In Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006. Association for Computing Machinery (ACM). 2006. p. 221-236. (Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06). doi: 10.1145/1173706.1173740

Roadmap for enhanced languages and methods to aid verification

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this