Semantics and Verification of Object-Oriented Languages


NII Shonan Meeting Seminar 063

Davide Ancona: Type soundness proofs with big-step operational semantics of object-oriented languages

Proofs of soundness of type systems are typically based on small-step operational semantics, because of the inability of big-step operational semantics to distinguish stuck from non-terminating computations.

In this talk I will present two techniques to prove type soundness with big-step semantics.

The former is based on the notion of coinductive big-step semantics, obtained by interpreting the semantics rules coinductively, and by considering non-well-founded values. The corresponding proof of soundness is rather involved, since it requires showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a specific distance function.

A simpler approach consists in approximating at arbitrary depth the possibly infinite derivations of the coinductive semantics with infinite sequences of finite derivations; in this way, type soundness can be proved by standard mathematical induction.

Finally, I will briefly discuss interesting research directions to overcome some of the limitations of the presented techniques.


Tachio Terauchi: Predicate Refinement Heuristics in Program Verification with CEGAR

Many of the modern program verifiers are based on the predicate abstraction with CEGAR method, The method looks for a sufficient inductive invariant to prove the given property of the given program by iteratively accumulating predicates that are obtained by analyzing spurious counterexamples, and predicate refinement heuristics like Craig interpolation are used for this purpose. In this talk, we overview our recent work on predicate refinement heuristics in CEGAR. Specifically, we show that a certain strategy for choosing predicates can guarantee the convergence of CEGAR at a modest cost. We also show that choosing small refinements guarantees fast convergence under certain conditions.


Erik Poll: State machine learning: from testing to formal specifications

Finite state machines are a great specification formalism: they are intuitive and simple to understand, and can be used to describe all sorts of systems, or properties of systems, that we want to verify.

Coming up with accurate state machine models can be a lot of work. However, state machine inference provides a great technique to automatically reverse-engineer application using just black-box testing.? This can provide formal models of existing code for free, as a useful first step to rigorous specification and then verification of this code. We will show this using case studies of bank cards, internet banking tokens, and TLS implementations.


Gary Leavens: Behavioral Subtyping, Specification Inheritance, and Modular Reasoning

This talk aims to characterize modular reasoning for object-oriented (OO) programs that use subtyping and dynamic dispatch. It gives a semantic characterization of supertype abstraction using two different semantics for a Java-like OO language. The first semantics is an accurate semantics of the language’s behavior. The second semantics mimics supertype abstraction, using static type information and method specifications to determine what a program should do. The validity of supertype abstraction is defined as having this second semantics accurately predict the behavior of programs with the dynamic semantics.

This talk is based on joint work with David A. Naumann of Stevens Institute of Technology, and is based on our paper “Behavioral Subtyping, Specification Inheritance, and Modular Reasoning” published in ACM TOPLAS, 37(4):13:1-13:88, Aug. 2015. (See The work of Gary Leavens was supported by NSF grants CNS-0808913, CCF-0916350, CCF-0916715, CCF-1017262, and CNS-1228695 David Naumann’s work was supported in part by NSF grants CCF-0915611 and CNS-1228930.


Hongseok Yang: ‘Cause I’m Strong Enough: Reasoning about Consistency Choices in Distributed Systems

Large-scale distributed systems often rely on replicated databases that allow a programmer to request different data consistency guarantees for different operations, and thereby control their performance. Using such databases is far from trivial: requesting stronger consistency in too many places may hurt performance, and requesting it in too few places may violate correctness. To help programmers in this task, we propose the first proof rule for establishing that a particular choice of consistency guarantees for various operations on a replicated database is enough to ensure the preservation of a given data integrity invariant. Our rule is modular: it allows reasoning about the behaviour of every operation separately under some assumption on the behaviour of other operations. This leads to simple reasoning, which we have automated in an SMT-based tool. We present a nontrivial proof of soundness of our rule and illustrate its use on several examples.

This is joint work with Alexey Gotsman (IMDEA, Spain),?Carla Ferreira (Universidade Nova Lisboa),?Mahsa Najafzadeh (UPMC & INRIA), and?Marc Shapiro (UPMC & INRIA).


Sukyoung Ryu: Analyzing JavaScript Web Applications in the Wild (Mostly) Statically

Analyzing real-world JavaScript web applications is a challenging task. On top of understanding the semantics of JavaScript, it requires modeling of web documents, platform objects, and interactions between them. Not only JavaScript itself but also its usage patterns are extremely dynamic. Most of web applications load JavaScript code dynamically, which makes pure static analysis approaches inapplicable. We present our attempts to analyze JavaScript web applications in the wild mostly statically using various approaches to analyze libraries.


Nadia Polikarpova: A Fully Verified Container Library

The comprehensive functionality and flexible design of general-purpose container libraries pose nontrivial challenges to formal verification. In this talk I will present our experience using the AutoProof program verifier to prove full functional correctness of a realistic container library. I will discuss the key ingredients of AutoProof’s methodology, which made the verification possible with moderate annotation overhead and good performance.


Tutorial by Werner Dietl: Preventing Errors Before They Happen

Are you tired of null pointer exceptions, unintended side effects, SQL injections, concurrency errors, mistaken equality tests, and other runtime errors? Are your users tired of them in your code? This presentation shows you how to guarantee, at compile time, that these runtime exceptions cannot occur. You have nothing to lose but your bugs!


Xin Li: Automata-Based Abstraction Refinement for muHORS Model Checking

The model checking of higher-order recursion schemes (HORS), aka. higher-order model checking, is the problem of checking whether the tree generated by a given HORS satisfies a given property. It has recently been studied actively and applied to automated verification of higher-order programs. Kobayashi and Igarashi studied an extension of higher-order model checking called ?HORS model checking, where HORS has been extended with recursive types, so that a wider range of programs, including object-oriented programs and multi-threaded programs, can be precisely modeled and verified. Although the ?HORS model checking is undecidable in general, they developed a sound but incomplete procedure for ?HORS model checking. Unfortunately, however, their procedure was not scalable enough. Inspired by recent progress of (ordinary) HORS model checking, we propose a new procedure for ?HORS model checking, based on automata-based abstraction refinement. We have implemented the new procedure and confirmed that it often outperforms the previous procedure.


Hiroshi Unno: Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types

In this talk, I will present a verification method for object-oriented programs in Featherweight Java (FJ) based on a transformation to functional programs in ML. The transformation encodes objects and dynamic method dispatching in FJ using higher-order functions and recursive data types in ML. The transformed programs are then verified by using the state-of-the-art techniques for ML programs such as refinement types, Horn clause solving, and higher-order model checking. In the talk, I will explain one of the techniques called refinement type optimization which we have proposed in SAS 2015.