**Vitor Santos Costa***, Associate Research Professor, University ofPorto, Portugal*

**Abstract:**

Prolog is an expressive declarative language, and it is the ideal language for learning from structured and complex data. I present some applicatiions of Prolog in this area. First, I iwll discuss applications in the medical domain, such as breast cancer and adverse drug reactions. I will then discuss more complex applications in computational chemistry and in forestry management. To conclude, I'll go back to the early days of logic programming and discuss the initial steps of an application where Prolog is used together with statistical models to analyse blogs.

**Time and place:**

10:00am Amphitheatre H-1002

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Derek Dreyer***, Assistant Research Professor, Max Planck Institute for Software Systems, Germany*

**Abstract:**

Fine-grained concurrent data structures (or FCDs) reduce the granularity of critical sections in both time and space, thus making it possible for clients to access different parts of a mutable data structure in parallel. However, the tradeoff is that the implementations of FCDs are very subtle and tricky to reason about directly. Consequently, they are carefully designed to be *contextual refinements* of their coarse-grained counterparts, meaning that their clients can reason about them as if all access to them were sequentialized. In this work, we propose a new semantic model, based on Kripke logical relations, that supports direct proofs of contextual refinement in the setting of a type-safe high-level language.

The key idea behind our model is to provide a simple way of expressing the "local life stories" of individual pieces of an FCD's hidden state by means of *protocols* that the threads concurrently accessing that state must follow. By endowing these protocols with a simple yet powerful transition structure, as well as the ability to assert invariants on both heap states and specification *code*, we are able to support clean and intuitive refinement proofs for the most sophisticated types of FCDs, such as conditional compare-and-set (CCAS). In the talk, I will give a fairly informal, interactive presentation of our proof method, looking at several motivating examples and describing at a high level how our proof method helps in reasoning about these examples. This is joint work with Aaron Turon, Jacob Thamsborg, Amal Ahmed and Lars Birkedal.

**Time and place:**

11:00am UPM Languages departament meeting room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Judith Bishop***, Researcher, Microsoft Research*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Roberto Di Cosmo***, Professor, Universite Paris Diderot, Director IRILL*

**Abstract:**

**Time and place:**

4:00pm IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Jan Reineke***, Assistant Professor, Saarland University, Germany*

**Abstract:**

Interaction of embedded systems with their physical environment often imposes timing constraints on the embedded system's software tasks. A key step in verifying that these constraints are met is to perform worst-case execution time (WCET) analysis of the software tasks. WCET analyses rely on detailed timing models of the execution platform. The development of timing models of modern execution platforms is a time-consuming and error-prone process that furthermore has to be repeated for every new execution platform. We propose to reverse this process:

1. Start by developing a timing model that enables precise and efficient WCET analysis, which can be developed once and for all.

2. Then develop different execution platforms conforming to this model. To allow for a wide range of efficient execution platforms, such a timing model can be parameterized in different architectural aspects, as for instance the sizes of different levels of the memory hierarchy and their respective latencies.

In this talk, I will present a class of such parameterized timing models and a precise parametric WCET analysis technique that can be applied to this class of models.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Kathryn Francis***, PhD Student, The University of Melbourne, Australia*

**Abstract:**

The field of Constraint Programming (CP) is concerned with solving combinatorial optimisation problems, and the associated tools have been successfully applied to large-scale problems in industry. Unfortunately, these tools are very difficult and inconvenient for general software developers to use, so many smaller problems which should be easily solved by CP technology are still tackled by hand or using ad-hoc algorithms.

Existing CP tools require the use of a separate paradigm to define the optimisation problem. This is true even for CP libraries embedded in general purpose programming languages. We suggest an alternative interface to CP which instead uses the semantics of the host language to define the problem. The programmer writes a procedure which constructs a solution using an oracle to make decisions, and another procedure which evaluates a solution. Both of these can make use of existing code and data types. The optimisation problem is to find the decisions which should be made by the oracle in order to maximise or minimise the evaluation result.

Using this procedure-based problem definition, optimisation can be seamlessly integrated into a wider application. During program execution optimisation is triggered be specifying the relevant procedures. An appropriate conventional constraint model is created automatically and sent to an external solver. Then the results are used to update the program state as though the procedure to build a solution has been executed with optimal decisions made by the oracle.

In this talk I will describe our prototype implementation of such an interface for Java.

**Time and place:**

12:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Jérôme Feret***, Researcher, École Normale Supérieure, France*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Geoffrey Smith***, Associate Research Professor, Florida International University, USA*

**Abstract:**

In this talk we discuss several recent results about min-entropy leakage. We first briefly recall the definitions of min-entropy leakage and min-capacity, and describe their basic properties. Next we consider several forms of channel composition: cascading, repeated independent runs, and adaptive composition. For each, we give bounds on the leakage of a composed channel in terms of the leakage of its constituents. Finally, we discuss two-bit patterns, a static analysis technique for computing upper bounds on the min-capacity of deterministic imperative programs; the idea is to determine what patterns hold for each pair of bits in the program's output, and then to use these patterns to bound the number of possible output values.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Diego Garbervetsky***, Professor, Universidad de Buenos Aires and CONICET, Argentina*

**Abstract:**

There is an increasing interest in understanding and analyzing the use of resources in software and hardware systems. Certifying memory consumption is vital to ensure safety in embedded systems as well as proper administration of their power consumption; understanding the number of messages sent through a network is useful to detect performance bottlenecks or reduce communication costs, etc. Assessing resource usage is indeed a cornerstone in a wide variety of software-intensive system ranging from embedded to Cloud computing. It is well known that inferring, and even checking, quantitative bounds is difficult (actually undecidable). Memory consumption is a particularly challenging case of resource-usage analysis due to its non-accumulative nature. Inferring memory consumption requires not only computing bounds for allocations but also taking into account the memory recovered by a GC.

In this talk I will present some of the work our group have been performing in order to automatically analyze heap memory requirements. In particular, I will show some basic ideas which are core to our techniques and how they were applied to different problems, ranging from inferring sizes of memory regions in real-time Java to analyzing heap memory requirements in Java/.Net. Then, I will introduce our new compositional approach which is used to analyze (infer/verify) Java and .Net programs. Finally, I will explain some limitations of our approach and discuss some directions for future research.

**Time and place:**

11:00am DLSIIS Meeting Room

Facultad de Informática, Bloque 2, room D-2319

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Geoffrey Smith***, Associate Research Professor, Florida International University, USA*

**Abstract:**

This talk introduces g-leakage, a rich generalization of the min-entropy model of quantitative information flow. In g-leakage, the benefit that an adversary derives from a certain guess about a secret is specified using a gain function g. Gain functions allow a wide variety of operational scenarios to be modeled, including those where the adversary benefits from guessing a value close to the secret, guessing a part of the secret, guessing a property of the secret, or guessing the secret within some number of tries. We discuss important properties of g-leakage, including bounds between min-capacity, g-capacity, and Shannon capacity. We also show a deep connection between a strong leakage ordering on two channels, C_1 and C_2, and the possibility of factoring C_1 into C_2 C_3 , for some C_3 . Based on this connection, we propose a generalization of the Lattice of Information from deterministic to probabilistic channels.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Pietro Ferrara***, Post-doctoral Researcher, ETH Zurich, Switzerland*

**Abstract:**

Effective static analyses must precisely approximate both heap structure and information about values. During the last decade, shape analysis has obtained great achievements in the field of heap abstraction. Similarly, numerical and other value abstractions have made tremendous progress, and they are nowadays effectively applied to the analysis of industrial software. In addition, several generic static analyzers have been introduced. These compositional analyzers combine many types of abstraction into the same analysis to prove various properties.

In this talk, we will present the combination of Sample, an existing generic analyzer, with a TVLA-based heap abstraction. First of all, we will introduce how Sample splits the heap abstraction from the value analysis. We will then present how we augment TVLA states with name predicates to identify nodes, and how we use TVLA as the engine to define the small step semantics of our analysis. Finally, we will sketch some preliminary experimental results.

**Time and place:**

13:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Mike Hicks***, Associate Research Professor, University of Maryland, USA*

**Abstract:**

Many useful programming constructions can be expressed as monads. Examples

include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In our previous work, we presented a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML’s built-in support for state and I/O. Developers write programs using monadic values of type m τ as if they were of type τ, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program typechecks.

A number of other programming idioms resemble monads but deviate from the standard monad binding mechanism. Examples include parameterized monads, monads for effects, information flow state tracking. Our present work aims to provide support for formal reasoning and lightweight programming for such constructs. We present a new expressive paradigm, polymonads, including the equivalent of monad and morphism laws.

Polymonads subsume conventional monads and all other examples mentioned above. On the practical side, we provide an extension of our type inference rewriting algorithm to support lightweight programming with polymonads.

Joint work with Nataliya Guts, Daan Leijen, and Nikhil Swamy

**Time and place:**

11:00am Amphitheatre H-1002

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Mike Dodds***, Post-doctoral Researcher, University of Cambridge, UK*

**Abstract:**

Disjointness between resources is an extraordinarily useful property when verifying concurrent programs. Threads that access mutually disjoint resources can be reasoned about locally, ignoring interleavings; this is the core insight behind Concurrent Separation Logic. However, concurrent modules often share resources internally, frustrating disjoint reasoning. In this talk, I will suggest that sharing is often irrelevant to the clients of these modules, and can be hidden. I will show how separation logic can be used to hide irrelevant sharing and recover disjoint reasoning.

**Time and place:**

10:45am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Earl Barr***, Post-doctoral Researcher, University of California at Davis, USA*

**Abstract:**

Natural languages like English are rich, complex, and powerful. The highly creative and graceful use of languages like English and Tamil, by masters like Shakespeare and Avvaiyar, can certainly delight and inspire. But in practice, given cognitive constraints and the exigencies of daily life, most human utterances are far simpler and much more repetitive and predictable. In fact, these utterances can be very usefully modeled using modern statistical methods. This fact has led to the phenomenal success of statistical approaches to speech recognition, natural language translation, question-answering, and text mining and comprehension.

We begin with the conjecture that most software is also natural, in the sense that it is created by humans at work, with all the attendant constraints and limitations—and thus, like natural language, it is also likely to be repetitive and predictable. We then proceed to ask whether a) code can be usefully modeled by statistical language models and b) such models can be leveraged to support software engineers. Using the widely adopted n-gram model, we provide empirical evidence supportive of a positive answer to both these questions. We show that code is also very repetitive, and in fact even more so than natural languages. As an example use of the model, we have developed a simple code completion engine for Java that, despite its simplicity, already improves Eclipse’s built-in completion capability. We conclude by laying out a vision for future research in this area.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Earl Barr***, Post-doctoral Researcher, University of California at Davis, USA*

**Abstract:**

Writing correct software is difficult; writing reliable numerical software involving floating-point numbers is even more difficult. Computers provide numbers with limited precision; when confronted with numbers that exceed that limit, they throw runtime exceptions or introduce approximation and error. Well-known studies (e.g., Huckle) show that numerical errors often occur and can be disastrous, even in "well-tested" code. Thus, practical techniques for systematic testing and analysis of numerical programs are much needed.

In this talk, I will present my recent work on developing testing and analysis techniques for numerical software. In particular, I will introduce Ariadne, the first practical symbolic execution engine for automatically detecting floating-point exceptions, and a novel testing framework that systematically perturbs a program's numerical calculations to elicit latent numerical instability. The tools have been extensively evaluated on the widely-used GNU Scientific Library (GSL). The results show that both tools are effective. In particular, Ariadne identified a large number of real, unchecked runtime exceptions in GSL. The GSL developers confirmed our preliminary findings and look forward to Ariadne's imminent public release.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Yuriy Brun***, Post-doctoral Researcher, University of Washington, USA*

**Abstract:**

Software developers primarily rely on experience and intuition to make development decisions. I will describe speculative analysis, a new technique that helps developers make better decisions by informing them of the consequences of their likely actions.

As a concrete example, I will consider collaborative development and the conflicts that arise when developers make changes in parallel. This is a serious problem. In industry, some companies hire developers solely to resolve conflicts. In open-source development, my historical analysis of over 140,000 versions of nine systems revealed that textual, compilation, and behavioral conflicts are frequent and persistent, posing a significant challenge to collaborative development. Speculative analysis can help solve this problem by informing developers early about potential and existing conflicts. Armed with this information, developers can prevent or more easily resolve the conflicts. I will demonstrate Crystal, a publicly available tool that detects such conflicts early and precisely. Crystal has inspired a collaboration with Microsoft and some Microsoft teams now use a version of the tool in their everyday work.

My research focuses on helping developers understand system behavior. By informing developers of the consequences of their choices, speculative analysis allows developers to understand the choices’ implications on the system’s behavior, leading to better decisions and higher-quality software. I will briefly describe three other results that help developers understand system behavior and then summarize my vision of how the mechanisms that inform developers can also be used to inform the system itself, allowing for self-adapting and self-managing systems.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Schmuel Mooly Sagiv***, Professor, Tel Aviv University, Israel*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

**Time and place:**

11:00am Amphitheatre H-1002

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Markus Rabe***, PhD Student, Saarland University, Germany*

**Abstract:**

Link: http://react.cs.uni-saarland.de/publications/DFKRS12.html

**Time and place:**

13:00am Amphitheatre H-1002

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

From a programming perspective, Alan Turing's epochal 1936 paper on computable functions introduced several new concepts and originated a great many now-common programming techniques. In particular, by treating programs as data, he invented the "universal machine", nowadays known as a self-interpreter.

We begin by reviewing Turing's contribution from a programming perspective; and systematise and mention some of the many ways that later developments in models of computation (MOCs) have interacted with computability theory and programming language research.

Next, we describe our 'blob' MOC: a recent biologically motivated stored-program computational model without pointers. Novelties of the blob model: programs are truly first-class citizens, capable of being automatically executed, compiled or interpreted. The model is Turing complete in a strong sense: a universal interpretation algorithm exists, able to run any program in a natural way and without arcane data encodings. The model appears closer to being physically realisable than earlier computation models. In part this owes to strong fi niteness due to early binding; and a strong adjacency property: the active instruction is always adjacent to the piece of data on which it operates.

**Time and place:**

11:00am Amphitheatre H-1002

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

**Neil Jones***, Professor, DIKU University of Copenhagen, Denmark*

**Abstract:**

Quick overview of: Interpreters, Compilers, and Program Specialisers

The Futamura projections (Futamura stated them; 13 years later DIKU achieved them on the computer):

- a partial evaluator can compile;
- a partial evaluator can generate a compiler;
- a partial evaluator can generate a compiler generator.

Underbar types to describe the Futamura projections: Types of interpreters, compilers, specialisers, and program self-application.

Partial evaluation: how it can be done, and measures of efficiency: Trivial program specialization. Interpretation overhead, including self-interpretation. How specialization can be done; binding-time analysis. Speedups from self-application in the Futamura projections. Optimal program specialization.

**Time and place:**

13:00 IMDEA conference room

Facultad de Informática, Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain