IMDEA initiative

Home > Events > Prev. Invited Talks

2012 Invited talks

Vitor Santos Costa

Wednesday, November 28, 2012

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

Learning with Prolog

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

Monday, November 19, 2012

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

Logical Relations for Fine-Grained Concurrency

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

Friday, November 16, 2012

Judith Bishop, Researcher, Microsoft Research

Microsoft research connecting to Labs and Academia

Abstract:

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


Roberto Di Cosmo

Tuesday, October 30, 2012

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

Analysing co-installability of software components

Abstract:

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


Jan Reineke

Thursday, October 25, 2012

Jan Reineke, Assistant Professor, Saarland University, Germany

Timing Analysis of Embedded Software for Platforms

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

Friday, October 19, 2012

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

Optimization modelling for software developers

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

Monday, October 15, 2012

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

Formal model reduction

Abstract:

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


Geoffrey Smith

Friday, June 22, 2012

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

Some Recent Results on Min-Entropy Leakage

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

Wednesday, June 20,2012

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

Quantitative analysis of Java/.Net like programs to understand heap memory requirements

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

Wednesday, June 13, 2012

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

Measuring Information Leakage using Generalized Gain Functions

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

Tuesday, June 12, 2012

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

TVLA and Value Analyses Together

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

Friday, June 1, 2012

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

Polymonads: reasoning and inference

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

Wednesday, May 23, 2012

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

Recovering Disjointness from Concurrent Sharing

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

Tuesday, May 22, 2012

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

On the Naturalness of Software (to appear at ICSE 2012)

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

Friday, April 18, 2012

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

Techniques and Tools for Engineering Robust Numerical Software

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

Thursday, April 12, 2012

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

Speculative Analysis: What's Wrong with the Program I Haven't Written Yet?

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

Monday, March 26, 2012

Schmuel Mooly Sagiv, Professor, Tel Aviv University, Israel

COLT: Testing and Verifying Atomicity of Composed Operations

Abstract:

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


Neil Jones

Friday, March 23, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

Some remarks on the spectrum problem

Abstract:

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


Neil Jones

Tuesday, March 21, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

Kleenes Second Recursion Theorem (Work in Progress)

Abstract:

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


Neil Jones

Wednesday, March 14, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

Superlinear speedup (Work in Progress)

Abstract:

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


Markus Rabe

Tuesday, March 13, 2012

Markus Rabe, PhD Student, Saarland University, Germany

Temporal Information Flow

Abstract:

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:
13:00am Amphitheatre H-1002
Facultad de Informática, Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain


Neil Jones

Wednesday, March 7, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

PROGRAMS = DATA = FIRST-CLASS CITIZENS IN A COMPUTATIONAL WORLD

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

Tuesday, February 22, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

Obfuscation by Partial Evaluation of Distorted Interpreters

Abstract:

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 sufficiently 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 flattening, 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


Neil Jones

Tuesday, February 14, 2012

Neil Jones, Professor, DIKU University of Copenhagen, Denmark

Introduction to partial evaluation

Abstract:

Quick overview of: Interpreters, Compilers, and Program Specialisers

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

  1. a partial evaluator can compile;
  2. a partial evaluator can generate a compiler;
  3. 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