Specifying and Verifying Advanced Control Features

By: Gary T. Leavens, David A. Naumann, Hridesh Rajan, and Tomoyuki Aotani

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.

ACM Reference

Leavens, G.T. et al. 2016. Specifying and Verifying Advanced Control Features. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA, Imperial, Corfu, Greece (2016), 80–96.

BibTeX Reference

@inproceedings{LeavensNaumannRajanAotani2016,
  author = {Gary T. Leavens and David A. Naumann and Hridesh Rajan and Tomoyuki Aotani},
  title = {Specifying and Verifying Advanced Control Features},
  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA, Imperial, Corfu, Greece},
  volume = {9953},
  series = {Lecture Notes in Computer Science},
  pages = {80--96},
  year = {2016},
  editor = {Tiziana Margaria and Bernhard Steffen},
  doi = {10.1007/978-3-319-47169-3_7},
  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.},
}