ECOOP

Soundness of type systems is an important property to guarantee the absence of certain kinds of runtime errors, that is, no false negatives can occur.

Unfortunately, for well-known theoretical limits, there are many programs that cannot be typed ...

Index refinements (or dependent types over a restricted domain) enable the expression of many desirable invariants that can be verified at compile time. We propose to incorporate a system of index refinements in a small, class-based, imperative, object-...

We present the Flyweight Object-Oriented (Fᴏᴏ) calculus for the modeling of object-oriented languages. Fᴏᴏ is a simple, minimal class-based calculus, modeling only essential computational aspects and emphasizing larger-scale features (e.g., inheritance ...

This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes ...

Specification languages have long featured ways to describe what does not change when an imperative procedure is executed: the so-called frame problem. Solutions to the frame problem are needed for formal verification in imperative programming, as ...

Regression verification and checking for illicit information flow in programs are probably the two most prominent instances of so-called relational program reasoning. Regression verification is concerned with proving that two programs behave either ...

Writing concurrent Java programs that provably terminate, i.e. that terminate in all executions allowed by the language specification, is difficult, because of the combination of two language "features": firstly, the virtual machine is allowed to throw ...

Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this ...