@inbook{338035180805454daff10c7d018920b5,
title = "Context-Aware Trace Contracts",
abstract = "The behavior of concurrent, asynchronous procedures depends in general on the call context, because of the global protocol that governs scheduling. This context cannot be specified with the state-based Hoare-style contracts common in deductive verification. Recent work generalized state-based to trace contracts, which permit to specify the internal behavior of a procedure, such as calls or state changes, but not its call context. In this article we propose a program logic of context-aware trace contracts for specifying global behavior of asynchronous programs. We also provide a sound proof system that addresses two challenges: To observe the program state not merely at the end points of a procedure, we introduce the novel concept of an observation quantifier. And to combat combinatorial explosion of possible call sequences of procedures, we transfer Liskov{\textquoteright}s principle of behavioral subtyping to the analysis of asynchronous procedures.",
author = "Reiner H{\"a}hnle and Eduard Kamburjan and Marco Scaletta",
note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",
year = "2024",
doi = "10.1007/978-3-031-51060-1\_11",
language = "English",
isbn = "978-3-031-51059-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "289--322",
booktitle = "Active Object Languages: Current Research Trends",
address = "Germany",
}