10:00am Amphitheatre H-1002

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

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

11:00am UPM Languages departament meeting room

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

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

11:00am IMDEA conference room

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

Microsoft research connecting to Labs and Academia

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

4:00pm IMDEA conference room

**Roberto Di Cosmo**, *Professor, Université Paris Diderot, France*

Modern software systems are built by composing components drawn from large repositories, whose size and complexity is increasing at a very fast pace.

A fundamental challenge for the maintainability and the scalability of such software systems is the ability to quickly identify the components that can or cannot be installed together: this is the co-installability problem, which is related to boolean satisfiability and is known to be algorithmically hard.

This joint work with Jerome Vouillon presents a novel approach to the problem, based on semantic preserving graph-theoretic transformations, that allows to extract from a concrete component repository a much smaller one with a simpler structure, but equivalent co-installability properties.

This smaller repository can be displayed in a way that provides a concise view of the co-installability issues in the original repository, or used as a basis for studying various problems related to co-installability, and in particular the evolution of co-installability during repository evolution.

This approach has been extensively tested on GNU/Linux distributions, but can be applied to a large class of component based systems.

**Time and place:**

4:00pm IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

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

12:00pm IMDEA conference room

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

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:00pm IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

Combinatorial explosion of protein states generated by post-translational modifications and complex formation. Rule-based models provide a powerful alternative to approaches that require an explicit enumeration of all possible molecular species of a system. Such models consist of formal rules stipulating the (partial) contexts for specific protein-protein interactions to occur. These contexts specify molecular patterns that are usually less detailed than molecular species. Yet, the execution of rule-based dynamics requires stochastic simulation, which can be very costly. It thus appears desirable to convert a rule-based model into a reduced system of differential equations by exploiting the lower resolution at which rules specify interactions.

In this talk, we present a formal framework for constructing coarse-grained systems. We track the flow of information between different regions of chemical species, so as to detect and abstract away some useless correlations between the state of sites of molecular species.

The result of our abstraction is a set of molecular patterns, called fragments, and a system which describes exactly the concentration (or population) evolution of these fragments. The method never requires the execution of the concrete rule-based model and the soundness of the approach is described and proved by abstract interpretation.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

**Carroll Morgan**, *Research Professor, University of New South Wales, Australia*

Noninterference security (due to Goguen and Meseguer) considers breaches that result from the -interference- that hidden (high security) data might cause, via a computer system, to visible (low security) data. Attackers can then observe the visible values and, from that, infer properties of the hidden values. Program algebra is an approach to designing correct software in which source-level program texts are manipulated in correctness preserving (or enhancing) ways, usually to take a specification (eg an inefficient one) to an implementation (more efficient) --- one that is as good as the specification, or better, according to properties agreed-on beforehand.

Program algebra for noninterference security thus begins with very simple, direct specifications such as "reveal the exclusive-or of three secret Booleans without revealing them individually" (as in Chaum's Dining Cryptographers protocol). Then via correctness-preserving source-level steps, it is transformed into an actual implementable protocol involving flips of secret coins.

The talk will explain and illustrate this kind of construction as it applies to noninterference security, and then briefly look at the mathematical machinery [1,2,3] that makes it possible.

The following are available at http://www.cse.unsw.edu.au/~carrollm/probs/

[1] The Shadow Knows. Carroll Morgan. Science of Computer Programming
74(8):629-53. 2009.

[2] Compositional closure for Bayes Risk in probabilistic
noninterference. McIver, Meinicke, Morgan. Proc ICALP 2010 (Part II),
223-35. 2010.

[3] A Kantorovich-Monadic Powerdomain for Information Hiding, with
Probability and Nondeterminism. McIver, Meinicke, Morgan. Proc LiCS
2012.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

12:00am IMDEA conference room

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

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:**

12:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

14:00am IMDEA conference room

**Heiko Mantel**, *Professor, TU Darmstadt, Germany*

Research on certifying information flow security for sequential programs has made much progress over the last fifteen years, resulting in elegant security properties, sound verification techniques and efficient analysis tools. It would be very desirable to adopt these techniques for the analysis of concurrent programs. Analysing the security of individual threads is, however, not sufficient for ensuring the security of concurrent programs. For sound compositional reasoning, the environment of a thread must be taken into account. So far, overly conservative approximations of environments have led to rather restrictive analyses, and this imprecision constitutes a major obstacle for the migration of information flow analysis into practice.

The overall goal of our project is to lift information flow analyses for concurrent programs to a similar level of precision as analyses for sequential programs. In the talk, I will present solutions for approximating the environment of individual threads more precisely, and I will demonstrate that this substantially increases the precision of information flow analyses for concurrent programs.

**Time and place:**

14:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am DLSIIS Meeting Room

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

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

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

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

1:00pm IMDEA conference room

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

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:**

1:00pm IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am Amphitheatre H-1002

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

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

10:45am IMDEA conference room

**Mike Dodds**, *Post-doctoral Researcher, University of Cambridge, United Kingdom*

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

11:00am IMDEA conference room

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

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

11:00am IMDEA conference room

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

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

11:00am IMDEA conference room

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

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

11:00am IMDEA conference room

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

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permit the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. It is easy to incorporate data representations synthesized by our compiler into existing systems, leading to code that is simpler, correct by construction, and comparable in performance to the code it replaces.

I will also describe the extension to generate fine-grain concurrent implementations.

This is a joint work with Peter Hawkins, Alex Aiken, Kathleen Fisher, and Martin Rinard. It appears in PLDI'11 and PLDI'12 articles. More information is available from here.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

In the last two decades, program verification and testing have gone a long way from a concept to practical tools which can be applied to real software. I will present a recent PhD thesis by Ohad Shacham which develops practical techniques for testing and verifying atomicity of composed collection operations. The techniques have been implemented in a tool (COLT) and successfully applied to uncover many bugs in real software. In fact, the Java library is currently being modified to avoid some of the bugs found by COLT. The effectiveness of COLT comes from an understanding of the interface requirements and using them to shorten the executed traces, avoiding superfluous traces which cannot uncover new violations.

COLT can also effectively prove the absence of atomicity violations for composed map operations. The main idea is to bound the number of keys and values that must be explored. This relies on restricting composed operations to be data-independent. That is, the control-flow of the composed operation does not depend on specific input values. While verifying data-independence is undecidable in the general case, we provide simple sufficient conditions that can be used to establish a composed operation as data-independent. We show that for the common case of concurrent maps, data-independence reduces the hard problem of verifying linearizability into a verification problem that can be solved efficiently using a bounded number of keys and values.

This is a joint work with Ohad Shacham, Eran Yahav, Alex Aiken, Nathan Bronson, and Martin Vechev.. Part of this work is published in OOPSLA'11.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

Scholz posed in 1952 the problem of characterising the class of spectra (of formulas in first-order logic with equality), and there soon after came interesting related questions by Asser, Bennett, Mostowski, etc. In the early 1970s Alan Selman and I discovered an exact characterisation of spectra.

The problem interested me because of its similarity to the "LBA problem" then widely studied in theoretical computer science. Spectra had properties very similar to the context-sensitive languages, and I began with the hypothesis that they were the same class. The correct answer turned out to be different, that spectra equal NEXPTIME. This result was in a way a product of its time, since this characterisation of "the spectrum problem" would not have been naturally expressible prior to the the development in the late 1960s by Hartmanis, Stearns and others of time- and space-bounded complexity classes.

Since then a wide range of research has been done in finite model theory, datalog, programming languages and "implicit complexity", to name a few closely related topics. From my computer science background a natural next question was: what is the expressive power of various subrecursive programming languages on finite input data structures? This brings up questions of the effects of imposing limits on both stored data, and on control structures. The talk will conclude with an array of results (many obtained by others), point out some regularities, and a tantalising fact (in my opinion) that is still not satisfactorily understood: that primitive recursion as a control structure seems to be inherently less expressive than general recursion or even tail recursion.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am IMDEA conference room

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

Self-adjusting computation is a language-based approach to writing incremental
programs that respond dynamically to input changes by maintaining a trace of the
computation consistent with the input, thus also updating the output. For
monotonic programs, i.e., where localized input changes cause localized changes
in the computation, the trace can be repaired efficiently by insertions and
deletions. However, non-local input changes can cause major reordering of the
trace; in such cases, updating the trace can be asymptotically equal to running
from scratch. We show how to eliminate the monotonicity restriction by
generalizing the update mechanism to use trace slices, which are partial
fragments of the computation that can be reordered with some bookkeeping.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am Amphitheatre H-1002

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

Many interesting program transformations (by Burstall-Darlington, Bird, Pettorossi, and many others) have been published that give superlinear program speedups on some program examples. However, these techniques seem all to require a "Eureka step" where the transformer understands some essential property relevant to the problem being solved (e.g., associativity, commutativity, occurrence of repeated subproblems, etc.). Such transformations have proven to be very difficult to automate.

On the other hand, fully automatic transformers exist, including: classical compiler optimisations, deforestation, partial evaluation and Turchin's supercompilation. However these can be seen only to yield linear time improvements. For example, a limit in string pattern matching was until recently to achieve the speedup of the Knuth-Morris-Pratt algorithm. (The KMP speedup is still linear, although its constant coefficient can be proportional to the length of the subject pattern.)

In 2007 Geoff Hamilton showed that his "distillation" transformation (a further development of supercompilation) can sometimes yield superlinear speedups. It has automatically transformed the quadratic-time "naive reverse" program, and the exponential-time "Fibonacci" program, each into a linear-time equivalent program that uses accumulating parameters. On the other hand, distillation works with a higher-order source language; and is a very complex algorithm, involving positive information propagation, homeomorphic embedding, generalisation by tree matching, and folding). It is not yet clear which programs can be sped up so dramatically, and when and why this speedup occurs.

My current work (joint with Hamilton) is to discover an essential "inner core" of distillation. One approach is to study simpler program classes that allow superlinear speedup. Surprisingly, asymptotic speedups can sometimes be obtained even for first-order tail recursive programs (in other words, imperative flowcharts). The most natural example (discovered just recently) transforms the natural factorial sum program for f(n) = 1! + 2! +...+ n! from quadratic time to linear time.

A disclaimer: we work in a simple imperative program context: no caches, parallelism, etc.

Some examples that suggest principles to be discovered and automated:

In functional programs:

- finding shared subcomputations (e.g., the Fibonacci example)
- finding unneeded computations (e.g., most of the computation done by "naive reverse")

In imperative programs:

- finding unneeded computations (e.g., generalising the usual compiler "dead code" analysis can give quadratic speedups)
- finding shared subcomputations (e.g., the factorial sum example)
- code motion to move an entire nested loop outside an enclosing loop
- strength reduction
- common subexression elimination across loop boundaries, eg extending "value numbering"

Alas, these principles seem to be buried in the complexities of the distillation algorithm and the subtleties of its input language. One goal of our current work is to extract the essential transformations involved, ideally to be able to extend classical compiler optimisations (currently able only to yield small linear speedups) to a well-understood and automated "turbo" version that achieves substantially greater speedups.

**Time and place:**

11:00am Amphitheatre H-1002

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

1:00pm Amphitheatre H-1002

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

Most analysis methods for information flow properties, such as noninterference, do not consider temporal restrictions. In practice, however, such properties rarely occur statically, but have to consider constraints such as when and under which conditions a variable has to be kept secret. I will present recent results on how to integrate information flow properties into linear-time temporal logics by introducing a new modal operator. Finally, I will sketch upcoming work on integrating information flow properties in game logics such as ATL*.

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

**Time and place:**

1:00pm Amphitheatre H-1002

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

11:00am Amphitheatre H-1002

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

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

11:00am IMDEA conference room

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

How to construct a general program obfuscator? We present a novel
approach to automatically generating obfuscated code P' from a program
P with source clear code. Start with a (program-executing) interpreter
interp for the language in which P is written. Then "distort" interp
so it is still correct, but its specialization P' with respect to P is
transformed code that is equivalent to the original program, but
harder to understand or analyze. A systematic approach to deformation
is to make program P obscure by transforming it to P' on which
(abstract) interpretation is incomplete. Interpreter distortion can be
done by making residual in the specialization process sufﬁciently many
interpreter operations to defeat an attacker in extracting sensible
information from transformed code. Potency of the obfuscator is proved
with respect to a general model of the attacker, modeled as an
approximate (abstract) interpreter. Our method is applied to: code
ﬂattening, data-type obfuscation, and opaque predicate insertion. The
technique is language independent and can be exploited for designing
obfuscating compilers.

**Time and place:**

11:00am IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain

1:00pm IMDEA conference room

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

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:**

1:00pm IMDEA conference room

Facultad de Informática

Universidad Politécnica de Madrid

28660-Boadilla del Monte, Madrid, Spain