Specifying and verifying advanced control features

Gary T. Leavens; David Naumann; Hridesh Rajan; Tomoyuki Aotani

doi:10.1007/978-3-319-47169-3_7

Specifying and verifying advanced control features

Gary T. Leavens, David Naumann, Hridesh Rajan, Tomoyuki Aotani

Department of Computer Science

Tokyo Institute of Technology

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

2 Scopus citations

Abstract

Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publication	Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings
Editors	Bernhard Steffen, Tiziana Margaria
Pages	80-96
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-319-47169-3_7
State	Published - 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9953 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

Greybox specification
JML language
Modular verification

Access to Document

10.1007/978-3-319-47169-3_7

Cite this

Leavens, G. T., Naumann, D., Rajan, H., & Aotani, T. (2016). Specifying and verifying advanced control features. In B. Steffen, & T. Margaria (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings (pp. 80-96). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9953 LNCS). https://doi.org/10.1007/978-3-319-47169-3_7

Leavens, Gary T. ; Naumann, David ; Rajan, Hridesh et al. / Specifying and verifying advanced control features. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings. editor / Bernhard Steffen ; Tiziana Margaria. 2016. pp. 80-96 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{847717c887f44bc4b07961f871b4b668,

title = "Specifying and verifying advanced control features",

abstract = "Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.",

keywords = "Greybox specification, JML language, Modular verification",

author = "Leavens, {Gary T.} and David Naumann and Hridesh Rajan and Tomoyuki Aotani",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.",

year = "2016",

doi = "10.1007/978-3-319-47169-3_7",

language = "English",

isbn = "9783319471686",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "80--96",

editor = "Bernhard Steffen and Tiziana Margaria",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

}

Leavens, GT, Naumann, D, Rajan, H & Aotani, T 2016, Specifying and verifying advanced control features. in B Steffen & T Margaria (eds), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9953 LNCS, pp. 80-96. https://doi.org/10.1007/978-3-319-47169-3_7

Specifying and verifying advanced control features. / Leavens, Gary T.; Naumann, David; Rajan, Hridesh et al.
Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings. ed. / Bernhard Steffen; Tiziana Margaria. 2016. p. 80-96 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9953 LNCS).

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

TY - GEN

T1 - Specifying and verifying advanced control features

AU - Leavens, Gary T.

AU - Naumann, David

AU - Rajan, Hridesh

AU - Aotani, Tomoyuki

N1 - Publisher Copyright: © Springer International Publishing AG 2016.

PY - 2016

Y1 - 2016

N2 - Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.

AB - Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.

KW - Greybox specification

KW - JML language

KW - Modular verification

UR - http://www.scopus.com/inward/record.url?scp=84994048432&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994048432&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-47169-3_7

DO - 10.1007/978-3-319-47169-3_7

M3 - Conference contribution

AN - SCOPUS:84994048432

SN - 9783319471686

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 80

EP - 96

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Steffen, Bernhard

A2 - Margaria, Tiziana

ER -

Leavens GT, Naumann D, Rajan H, Aotani T. Specifying and verifying advanced control features. In Steffen B, Margaria T, editors, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Proceedings. 2016. p. 80-96. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-47169-3_7

Specifying and verifying advanced control features

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Cite this