Informatics Seminar Series by Prof. Éric Tanter

The Faculty of Informatics is pleased to announce a series of seminars given by Éric Tanter, University of Chile

TITLE: Summarized Trace Indexing and Querying for Scalable Back-in-Time Debugging [ECOOP 2011]
DATE: Friday, July 22nd, 2011
PLACE: USI Università della Svizzera italiana, room SI-006, Black building (Via G. Buffi 13)
TIME: 14.30

ABSTRACT:
Back-in-time debuggers offer an interactive exploration interface to execution traces.
However, maintaining a good level of interactivity with large execution traces is challenging. Current approaches either maintain execution traces in memory, which limits scalability, or perform exhaustive on-disk indexing, which is not efficient enough. We present a novel scalable disk-based approach that supports efficient capture, indexing, and interactive navigation of arbitrarily large execution traces.
In particular, our approach ensures strong guarantees in terms of query processing time, ensuring an interactive debugging experience. The execution trace is divided into bounded-size execution blocks about which summary information is indexed.
Blocks themselves are discarded, and retrieved as needed through partial deterministic replay. For querying, the index provides coarse answers at the level of execution blocks, which are then replayed to find the exact answer. Benchmarks on a prototype for Java show that the system is fast in practice, and outperforms existing back-in-time debuggers.

---

TITLE: The Sixth Sense: Programming with Ghosts
DATE: Monday, July 25th, 2011
PLACE: USI Università della Svizzera italiana, room SI-008, Black building (Via G. Buffi 13)
TIME: 11.00

ABSTRACT:
Development environments do not really support the kind of incremental development that programmers rely on. Frequently, either following test-driven development principles or incrementally refining an existing class, programmers code against a class or interface that is not (fully) defined yet. IDEs get in the way by showing off many error messages, especially in the case of statically-typed languages like Java and C#. On the one hand, ignoring these messages prevents the programmer from getting feedback from the IDE regarding potential inconsistencies and typing errors.
On the other hand, attending these error messages breaks the workflow of the programmer. We recognize that these not-yet-defined entities actually exist (in the programmer's mind) before they exist (in the IDE): like ghosts, only few gifted ones can see them. In order to smoothly support incremental development, we propose to extend IDEs with support for ghost classes and members. Ghosts are reified in the IDE, where they are built transparently and non-intrusively.
A dedicated ghost view allows programmers to check their ghosts and bust them into actual code when ready. At the programming language level, we show how to extend traditional type systems to support ghosts and report inconsistencies among ghosts early on.

---

TITLE: Computational Contracts: Grey Box Verification and Blame Assignment in a Higher-Order Setting
DATE: Monday, July 25th, 2011
PLACE: USI Università della Svizzera italiana, room SI-008, Black building (Via G. Buffi 13)
TIME: 15.45

ABSTRACT:
Pre/post contracts for higher-order functions, as proposed by Findler and Felleisen and provided in Racket, allow run-time verification and blame assignment of higher-order functions. However these contracts treat contracted functions as black boxes, allowing verification of only input and output. It turns out that many interesting concerns about the behavior of a function require going beyond that black-box approach, in order to control the actual computation that follows from a function. Examples are prohibiting or verifying that certain functions are called, checking access permissions, time or memory constraints, interaction protocols, etc.
To address this need for grey-box verification, while preserving support for higher-order programming and blame assignment, we introduce the notion of computational contracts. A computational contract is a contract over the execution of a contracted entity. We show various applications of computational contracts, and explain how to assign blame in case of a violation. Computational contracts have been integrated with the existing contract system of Racket. Computational contracts is the first contract model with blame assignment in a higher-order setting that provides a systematic way to perform grey box verification.

BIO:
Éric Tanter is an Associate Professor in the Computer Science Department of the University of Chile, where he co-leads the PLEIAD laboratory. His research focuses on various dimensions of programming languages and paradigms, from foundations to applications to software engineering issues. Most crucially, he aims at reconciling flexibility and safety in programming. He holds a PhD from the University of Nantes and University of Chile (2004).

HOST: Prof. Walter Binder