Context-aware Trace Contracts

ABSTRACT

The behavior of concurrent, asynchronous procedures depends in general on the call context, because of the global protocols that govern 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 internal behavior of a procedure, such as calls or state changes, but not its call context. In this talk we discuss 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: First, to observe the program state not merely at the end points of a procedure, we introduce the novel concept of an observation event. Second, to combat combinatorial explosion of possible call sequences of procedures, we adapt Liskov’s principle of behavioral subtyping to the analysis of asynchronous calls. This is a joint work with Eduard Kamburjan (U Oslo) and Marco Scaletta (TU Darmstadt).

SHORT BIO:

Reiner Hähnle is Professor in Software Engineering at the Computer Science Department of TU Darmstadt. He has wide-ranging interests in the formal foundations of software design, programming languages, and quality assurance by verification. He is co-initiator of the KeY project that maintains the well-known, eponymous Java verification tool, and he is co-designer of the active object language ABS. Moreover, he is co-founder of the Tableaux and IJCAR conference series and currently SC Chair of FASE.

Notably, he was the first ever Wine Chair of an international Computer Science conference at ECOOP 2014.