No.063 Semantics and Verification of Object-Oriented Languages

Icon

NII Shonan Meeting Seminar 063

Alex Summers: The Viper Project: Verification Infrastructure for Permission-based Reasoning

Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade. However, verification approaches geared around complex program logics (such as separation logic) have typically been implemented in specialised tools, since the reasoning is hard to map down to first-order automated reasoning. In practice, this means that a rich variety of modern techniques have no corresponding tool support.

In this talk, I will present the new Silver intermediate verification language, which has been designed to facilitate the lightweight implementation of a variety of modern methodologies for program verification. In contrast to lower-level verification languages, Silver provides native support for heap reasoning; modes of reasoning such as concurrent separation logic, dynamic frames and rely-guarantee/invariants can be simply encoded.

Silver has been developed as part of the Viper project, which provides two automated back-end verifiers for Silver programs. Since releasing our software in September last year, it has been used for (internal and external) projects to build tools for Java verification, non-blocking concurrency reasoning, flow-sensitive typing and reasoning about GPU and Linux kernel code.

Slides

Comparing OO verification techniques

Julian Rathke: Compositional Reachablility in Petri Nets

We consider a compositional approach to deciding reachability for 1-bounded Petri Nets. We introduce a novel notion of Petri Nets with boundaries in order to capture the requirements on interactions between the composed subnets. This approach allows for a new divide and conquer style algorithm for the problem. We also describe a tool based implementation of the approach and compare its performance against other state-of-the-art reachability checkers.

Slides

Rustan Leino: Traits and dynamic frames

Dafny is a verification-aware programming language [0]. It includes instantiable classes that can be reasoned about using the _dynamic frames_ specification idiom. Previously, there was no inheritance among classes, but a recent addition to the language added _traits_ [1], which are abstract subperclasses with fields, functions, and methods. In this talk, I describe the traits in Dafny. I then give a tutorial on using dynamic frames and show how these are used with traits. I also mention some future work and bring up some questions I have about the design.

[0] K. Rustan M. Leino. Dafny: An automatic program veri?er for functional correctness. In LPAR-16, volume 6355 of LNAI, pages 348?370. Springer, April 2010.
[1] Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa. Automatic verification of Dafny programs with traits. FTfJP@ECOOP 2015: 4:1-4:5. July 2015.

Alex Potanin: Wyvern Formalisation

Wyvern is a new object-oriented programming language developed at CMU and VUW targeting web and mobile app developers concerned about security, safety, and productivity. In this talk, I will go over our current state of formalisation of different aspects of Wyvern starting with a simple core (extended Lambda Calculus) and moving through more complex stages adding objects, classes, and modules that translate back to the simpler cores. Finally, I will address the current major issues we are experiencing formalising Wyvern module system and security guarantees it can provide as well as formalising type members (as found in Scala or Beta) as we add them to Wyvern.

Slides

Vasileios Koutavas: Reasoning about Class Behavior using the Bisimulation Technique

In this talk we will discuss a proof technique for reasoning about contextual equivalence of classes in an imperative subset of Java. The technique is based on environmental bisimulations and is sound and complete with respect to contextual equivalence. We will see how inheritance and downcasting affect the technique, and explore example equivalent and inequivalent classes.

Slides

Steven Ramsay: Deciding contextual equivalence for IMJ*

I will describe joint work with Andrzej Murawski and Nikos Tzevelekos in which we consider the problem of deciding observational equivalence for IMJ*.? IMJ* is a kind of maximal fragment of the language Interface Middleweight Java (IMJ)?for which the problem is decidable. Given two, possibly open (containing free identi?ers), terms of IMJ*, the contextual equivalence problem asks if the terms can be distinguished by any possible IMJ context.? Our decision procedure reduces this problem to the emptiness problem for fresh-register pushdown automata.? I will demonstrate our implementation of the procedure in?the tool Coneqct.

slides

Nikos Tzevelekos: Game Semantics for Interface Middleweight Java

In this talk we present a denotational/operational model that captures the behaviour of programs written in an object calculus called IMJ and in which open terms interact with the environment through interfaces. The calculus is intended to represent the essence of contextual interactions of Middleweight Java code. The model is based on game semantics, a technique which models interactions between a program and its environment as formal games. Working with games, we build fully abstract models for the induced notions of contextual approximation and equivalence.

This is joint work with A. Murawski.

Slides

Atsushi Igarashi: Type Systems for Dynamic Layer Composition

Key features of context-oriented programming (COP) are _layers_—modules to describe context-dependent behavioral variations of a software system—and their _dynamic activation_, which can modify the behavior of multiple objects that have already been instantiated.? Typechecking programs written in a COP language is difficult because the activation of a layer can even change objects’ interfaces.

In this talk we present a few type systems to deal with such dynamic layer compositions.? Starting with a very simple but restrictive type system, we gradually add language features and extend the type system accordingly.

This is a joint work with Hiroaki Inoue, Robert Hirschfeld, and Hidehiko Masuhara.

Slides

Tomoyuki Aotani: A semantics for context-oriented programming languages with multiple layer activation mechanisms

Context-oriented programming (COP) is an approach to modularize behavioral variations of programs into layers from the viewpoint of contexts that change dynamically during the execution of a program. Changing behavior with respect to changes of contexts is achieved by activating or deactivating layers and dispatching methods according to not only the dynamic type of the receiver object but also the set of active layers. Several layer-activation mechanisms have been proposed separately for COP languages. In this talk we propose new semantics using monads and comonads for COP languages supporting multiple layer-activation mechanisms.

slides