## Invited Talks - 2014

### Friday, December 12, 2014

10:45am Meeting room 302 (Mountain View), level 3

Darko Stefanovic, Associate Professor, University of New Mexico, USA

### Playing robotics with DNA

#### Abstract:

Can we build molecular-scale devices that are justly called robots? A macroscopic robot has a large source of deterministic computational power that it uses to process the information from its sensors and guide its actuators. At the molecular scale there seems to be little computation available, while sensing and actuation are directly linked. Yet nature's molecular "motors" and "machines" in cells are responsible for maintaining life processes. To begin answering the question, we can take a synthetic approach, inspired by both the macroscopic robotics analogues and the biological analogues. I will review my involvement in the development of DNA-based computational circuits and walkers. I will also touch on the role of programming languages in this enterprise.

Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Tuesday, December 9, 2014

10:45am Meeting room 302 (Mountain View), level 3

Roberto Giacobazzi, Faculty (visiting), IMDEA Software Institute

### Obscuring code - Unveiling and Veiling Information in Programs

#### Abstract:

The talk concerns the design of code protecting transformations for white-box cryptography in a MATE (Man-At-The-End) attack scenario. The battle scenario involves attackers, modeled as approximate (abstract) interpreters of source programs intended to extract information about their run-time behavior, and protecting code transformations, modeled as distorted compilers devoted to inhibit attacks. Attacks are inhibited by maximizing imprecision (incompleteness) in all approximate computations made by the attacker. A brief overview on completeness in abstract interpretation (including recent achievements in POPL15) will set the theoretical background. The model is general enough to include generic static and dynamic attacks. Protecting transformations are systematically and formally derived as distorted compilers, by specializing a distorted interpreter for the programming language with respect to the source code to protect. Interestingly this distortion corresponds precisely to defeat the potency of the expected attacker, which consists in its ability to extract a complete and precise view of program's execution.

Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Thursday, October 30, 2014

11:00am Meeting room 302 (Mountain View), level 3

Michael Näf, ,

### The Doodle Story

#### Abstract:

Doodle (www.doodle.com) is the worldwide leader when it comes to online consensus-based scheduling. The service reaches more than 20 million users each month.

In this talk, the original founder of the project will cover some highlights and lessons learned along the way of building and monetizing a consumer product, and seeing a company through VC-funding, break-even, and exit.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Friday, October 17, 2014

11:00am Meeting room 302 (Mountain View), level 3

Dimitrios Vytiniotis, Researcher, Microsoft Research, Cambridge, UK

### Ziria: wireless programming for hardware dummies

#### Abstract:

Software-defined radio (SDR) brings the flexibility of software to the domain of wireless protocol design, promising both an ideal platform for research and innovation and the rapid deployment of new protocols on existing hardware. Most existing SDR platforms require careful hand-tuning of low-level code to be useful in the real world.

In this talk I will describe Ziria, an SDR platform that is both easily programmable and performant. Ziria introduces a programming model that builds on ideas from functional programming and that is tailored to wireless physical layer tasks. The model captures the inherent and important distinction between data and control paths in this domain. I will describe the programming model, give an overview of the execution model, compiler optimizations, and current work on parallelization and scheduling reconfigurable pipelines. We have used Ziria to produce an implementation of 802.11a/g and a partial implementation of LTE.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Thursday, October 2, 2014

11:00am Meeting room 302 (Mountain View), level 3

Amir Ben-Amram, Professor, Tel Aviv-Yaffo Academic College

### What is decidable in growth-rate analysis of programs?

#### Abstract:

Growth-rate analysis is the problem of finding, for a program in a suitable programming language, how fast the computed values, or the running time, etc., grow as a function of the input. We concentrate on decision problems like: do the values grow at most polynomially in the input? In this talk I will survey research starting with a CiE 2008 paper where Jones, Kristiansen and I presented an algorithm that, for a simple but non-trivial imperative programming language, answers the polynomial and linear growth-rate questions. The interesting part was that the algorithm solved the problem precisely---problems of this type are undecidable for ordinary, full languages, and even rather simple ones. The surprising part was that it ran in polynomial time. Consequently, we have tried to explore the boundaries of tractability and decidability in the vicinity of our original problem, that is, to consider modifications to the programming language and study their effect.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Tuesday, September 16, 2014

11:00am Lecture hall 1, level B

Hongseok Yang, Professor, University of Oxford, UK

### How to find a good program abstraction automatically?

#### Abstract:

Recent years have seen the development of successful commercial programming tools based on static analysis technologies, which automatically verify intended properties of programs or find tricky bugs that are difficult to detect by testing techniques. One of the key reasons for this success is that these tools use clever strategies for abstracting programs---most details about a given program are abstracted away by these strategies, unless they are predicted to be crucial for proving a given property about the program or detecting a type of program errors of interest. Developing such a strategy is, however, nontrivial, and is currently done by a large amount of manual engineering efforts in most tool projects. Finding a good abstraction strategy automatically or even reducing these manual efforts involved in the development of such a strategy is considered one of the main open challenges in the area of program analysis. In this talk, I will explain how I tried to address this challenge with colleagues in the past few years. During this time, we worked on parametric program analyses, where parameters for controlling the degree of program abstraction are expressed explicitly in the specification of the analyses. For those analyses, we developed algorithms for searching for a desired parameter value with respect to a given program and a given property, which use ideas from the neighbouring areas of program analysis such as testing, searching and optimisation. In my talk, I will describe the main ideas behind these algorithms without going into technical details. I will focus on intuitions about why and when these algorithms work. I will also talk briefly about a few lessons that I learnt while working on this problem. This talk is based on the joint work with Mayur Naik, Xin Zhang, Ravi Mangal, Radu Grigore, Ghila Castelnuovo and Mooly Sagiv.

Time and place:
11:00am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo

### Thursday, September 11, 2014

11:00am Meeting room 302 (Mountain View), level 3

Jan Midtgaard, Post-doctoral Researcher, Aarhus University, Denmark

### QuickChecking Static Analysis Properties

#### Abstract:

A static analysis can check programs for potential errors. A natural question that arises is therefore: who checks the checker? Researchers have given this question varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough soundness proofs by hand, to automated fixed point checking.

We demonstrate how quickchecking can be used to test a range of static analysis properties with limited effort. Our approach is twofold:

(1) we show how we can check a range of algebraic lattice properties --- to help ensure that an implementation follows the formal specification of a lattice, and

(2) we offer a number of generic, type-safe combinators to check transfer functions and operators between lattices --- to help ensure that these are, e.g., monotone, strict, or invariant.

We substantiate our claims by quickchecking a non-trivial type analysis for the Lua programming language.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Wednesday, July 30, 2014

12:00pm Meeting room 302 (Mountain View), level 3

Mihir Bellare, Professor, UC San Diego

### Caught between Theory and Practice

#### Abstract:

This talk explores the culture and motivations of the cryptographic research community. I examine the tension between theory and practice through the lens of my own experience in moving between them. I examine the peer review process through the lens of psychology and sociology. In both cases the aim is to go from critique to understanding and, eventually, change.

Time and place:
12:00pm Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, July 21, 2014

11:00am Meeting room 302 (Mountain View), level 3

Somesh Jha, Professor, University of Wisconsin, USA

### Retrofitting Legacy Code for Security

#### Abstract:

Writing a complex but secure program is a near-impossible task for a conventional operating system. If an attacker compromises any module of a trusted program running on such a system, then the attacker can perform arbitrary operations on the system. However, if a program runs on a privilege-aware operating system, then the program can invoke system calls to explicitly manage the privileges of its modules, and thus minimize the abilities of an attacker. The developers of privilege-aware systems have rewritten complex programs to invoke such system calls to satisfy strong security properties. However, such systems have not been adopted by developers outside the development community of each system. Moreover, even the systems' own developers often write programs for their system that they believe to be correct, only to realize later through testing that the rewritten program is insecure or does not demonstrate desired functionality of the original program. In this talk we will examine the challenges in rewriting programs for privilege-aware systems, and present a tool, called a policy weaver, that rewrites programs for such systems automatically. Our policy weaver takes as input a program written for a conventional system and a small and declarative policy (i.e., a regular expression describing allowed program executions). The weaver outputs a version of the program that invokes system calls so that it satisfies the policy. The weaver reduces each rewriting problem to finding a correct strategy to a two-player automata-theoretic safety game. We describe our experience developing a policy weaver for the Capsicum privilege-aware operating system (now included in FreeBSD 9.0), and describe how a policy weaver for an arbitrary privilege-aware system can be constructed automatically by providing a declarative model of the system to a policy-weaver generator.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, July 14, 2014

11:30am Meeting room 302 (Mountain View), level 3

Deepak Kapur, Research Professor, University of New Mexico, USA

### A Quantifier-Elimination Heuristic for Octagonal Constraints

#### Abstract:

Octagonal constraints expressing weakly relational numerical properties of the form ($l \le \pm x \pm y \leq h$) have been found useful and effective in static analysis of numerical programs. Their analysis serves as a key component of the tool ASTREE based on abstract interpretation framework proposed by Patrick Cousot and his group, which has been successfully used to analyze commercial software consisting of hundreds of thousand of lines of code. This talk will discuss a heuristic based on the quantifier-elimination (QE) approach presented by Kapur (2005) that can be used to automatically derive loop invariants expressed as a conjunction of octagonal constraints in $O(n^2)$, where $n$ is the number of program variables over which these constraints are expressed. This is in contrast to the algorithms developed in Mine's thesis which have the complexity at least $O(n^3)$. The restricted QE heuristic usually generates invariants stronger than those obtained by the freely available Interproc tool. Extensions of the proposed approach to generating disjunctive invariants will be presented.

Time and place:
11:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, July 7, 2014

11:30am Meeting room 302 (Mountain View), level 3

Colin Fleming, ,

### Cursive -- an IDE for Clojure Programming Language

#### Abstract:

In this talk Colin will give a brief introduction to Clojure, a JVM-based programming language from the Lisp family, as well as to IntelliJ -- a powerful integrated development environment for Java-like languages. He will then present Cursive -- an IntelliJ-based IDE for Clojure and discuss the implementation and the experience of developing Cursive in Clojure, as well as the challenges of developing an IDE for such a flexible language. He will also discuss how the static analysis approach used by Cursive differs from more traditional REPL-based environments (e.g., Emacs) and what the pros and cons of this approach are.

Time and place:
11:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Tuesday, July 15, 2014

11:00am Meeting room 302 (Mountain View), level 3

Jim Kapinski, Senior Research Engineer, Toyota Technical Center, Los Angeles, USA

### Simulation-Guided Analysis for Industrial Embedded Control Designs

#### Abstract:

Model-based development (MBD) is a popular technique for performing embedded control system design for cyber-physical systems, such as automotive control systems. MBD designs are used to generate critical software, so it is vital to ensure correctness of these designs, but verifying MBD designs is a difficult and expensive process. This talk presents some current research into simulation-guided approaches to evaluate whether MBD designs meet functional and performance requirements. We present a technique to perform Lyapunov analysis and to discover contraction metrics for nonlinear dynamical systems using information obtained from simulations of the system. We demonstrate how the technique can be applied to industrial systems with an automotive powertrain control example.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, June 23, 2014

10:30am Meeting room 302 (Mountain View), level 3

June Andronick, Senior Research Engineer, NICTA, Australia

### Formal proof of security for million-lines-of-code systems

#### Abstract:

Our vision to verify the security of large and complex systems is to: (i) design the system as a componentised, kernel-based system, with a minimal Trusted-Computing-Base, and (2) make use of the kernel's access control mechanism to isolate trusted components from untrusted parts, allowing to concentrate the verification effort on the trusted components. In this talk I will explain our work in turning this vision into a real, formally verified system. We are considering a multi-level terminal system, and the formal verification of the absence of unauthorised information and data flows. This work includes the development of a framework to minimize the manual proof effort required for each system. It leverages existing proofs of access control and information flow at the kernel level, in our case seL4, to automatically decompose the proof and only require manual proofs for the trusted components. The end goal is to provide a repeatable process for the design and verification of low-cost, high-assurance systems.

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Wednesday, June 18, 2014

10:30am Meeting room 302 (Mountain View), level 3

June Andronick, Senior Research Engineer, NICTA, Australia

### Trustworthy Systems at NICTA

#### Abstract:

In this talk, I will give an overview of the various current activities within NICTA's Trustworthy Systems team. Building on our work on seL4, we aim at providing unprecedented security, safety, reliability and efficiency for software systems. seL4 is a real-world, general-purpose operating system, with a guarantee that its machine code is correct with respect to its specification, and that it enforces critical security properties such as information flow control, integrity and authority confinement. Present activities focus on extending the safety and security properties of seL4, and extending the formal guarantees to user-level code, including automatic co-generation of code and proofs. For tightly constrained devices without memory protection, we are also working on verifying eChronos, a small real-time OS for embedded micro-controllers. Both seL4 and eChronos are used in a DARPA-funded project aiming at the demonstration of a complete high-assurance system and technology transfer to a real autonomous helicopter built by Boeing.

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, April 28, 2014

10:30am Meeting room 302 (Mountain View), level 3

Alessandra Gorla, Post-doctoral Researcher, Saarland University, Germany

### Improving the reliability of software systems using their intrinsic redundancy

#### Abstract:

Software is often redundant, in the sense that some operations are designed to behave like others but their executions differ. This redundancy can be introduced deliberately, as in the case of N-version programming, or it can be intrinsically present due to common design and development practices. I will present and discuss the notion of intrinsic redundancy and I will show that it exists and can be exploited to improve the reliability of software systems. I will first present a technique that uses such redundancy to automatically recover from runtime failures. I will then present another use of intrinsic redundancy to generate testing oracles.

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Friday, March 21, 2014

10:30am Meeting room 302 (Mountain View), level 3

Giordano Tamburrelli, PhD Student, Università della Svizzera Italiana, Lugano, Switzerland

### Models at run-time: open challenges and existing solutions

#### Abstract:

Research on model-driven engineering has mainly focused on the use of models during software development. This work has produced relatively mature techniques and tools that are currently being used in industry and academia to manage software complexity during development. Research on models at run-time seeks to extend the applicability of models and abstractions to the runtime environment, with the goal of providing effective technologies for managing the complexity of evolving software behaviour while it is executing. As is the case for many software development models, a runtime model is often created to support reasoning. However, in contrast to development models, runtime models are used to reason about the operating environment and runtime behaviour for some purpose, for example, to determine an appropriate form of runtime adaptation or reconfiguration. In this talk we will go trough some recent approaches for run-time models that support dynamic adaptation of systems with a particular emphasis on quantitative and probabilistic models. Beside describing these existing solutions, the talk also outlines a list of open challenges and shapes a potential future research agenda.

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Wednesday, March 12, 2014

10:30am Meeting room 302 (Mountain View), level 3

Hazem Torfah, PhD Student, Saarland University, Germany

### Counting Models of Linear-time Temporal Logic

#### Abstract:

We investigate the model counting problem for safety speci- ﬁcations expressed in linear-time temporal logic (LTL). Model counting has previously been studied for propositional logic; in planning, for example, propositional model counting is used to compute the plan’s robust- ness in an incomplete domain. Counting the models of an LTL formula opens up new applications in veriﬁcation and synthesis. We distinguish word and tree models of an LTL formula. Word models are labeled sequences that satisfy the formula. Counting the number of word models can be used in model checking to determine the number of errors in a system. Tree models are labeled trees where every branch satisﬁes the formula. Counting the number of tree models can be used in synthesis to determine the number of implementations that satisfy a given formula. We present algorithms for the word and tree model counting problems, and compare these direct constructions to an indirect approach based on encodings into propositional logic. <\p>

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Tuesday, March 11, 2014

10:30am Meeting room 302 (Mountain View), level 3

Domenico Bianculli, Researcher, Università della Svizzera Italiana, Lugano, Switzerland

### A Journey through Specification and Verification Techniques for Open-World Software

#### Abstract:

Open-world software systems are built by composing heterogeneous, third-party components, whose behavior and interactions cannot be fully controlled or predicted; moreover, the environment they interact with is characterized by frequent, unexpected, and welcome changes. An example of open-world software is represented by service-based applications, often realized by composing multiple services into a business process. Open-world software exhibits new features that demand for rethinking and extending the traditional methodologies and the accompanying methods and techniques. In this talk I will first illustrate SOLOIST, a specification language based on a new class of specification patterns, tailored for specifying both functional and quality-of-service properties of the interactions of service compositions. I will then present an approach for verifying SOLOIST properties over service execution traces using bounded satisfiability checking techniques. The talk will also touch upon the issues of making verification incremental and shifting it to run time. <\p>

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Thursday, March 6, 2014

10:30am Meeting room 302 (Mountain View), level 3

Julia Rubin, Researcher, Haifa Research Lab

### To Merge or Not to Merge: Managing Software Families

#### Abstract:

Software surrounds us and drives our lives: most modern systems heavily rely on software. Managing the complexity of these large software systems is a challenging task. It is even more challenging for software product lines -- families of software variants with similar yet not identical functionality (think Samsung's Galaxy S line which includes over two dozen smartphone models, each with its own variation of software). In the last two decades, numerous approaches have been proposed to help develop product lines in an efficient manner. Surprisingly, they are rarely used in practice. In this talk, we investigate reasons for such lack of adoption. We then propose an approach for improving existing practices that relies on a set of software analysis and transformation tasks. We show that some of the required tasks are barely studied by existing works and look in detail into one of them: matching artifacts from multiple products (a.k.a. n-way match). We explain why the n-way match problem is NP-hard, explore possible approximate solutions, and propose our own heuristic n-way match algorithm that is superior to other practical approaches in terms of its accuracy. We conclude the talk by outlining a future research agenda.

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Monday, February 24, 2014

10:30am Meeting room 302 (Mountain View), level 3

Chris Parnin, PhD Student, Georgia Institute of Technology, USA

### Programmer, Interrupted

#### Abstract:

Despite its vast capacity and associative powers, the human brain does not deal well with interruptions. Particularly in situations where information density is high, such as during a programming task, recovering from an interruption requires extensive time and effort. Although researchers recognize this problem, no programming tool takes into account the brain's structure and limitations in its design. In this talk, I describe my research collecting evidence about the impact of interruptions on programmers, understanding how programmers managed them in practice, and designing tools that can support interrupted programmers. I present a conceptual framework for understanding human memory organization and its strengths and weaknesses, particularly with respect to dealing with work interruptions. The framework explains empirical results obtained from experiments in which programmers were interrupted. For researchers, the intent is to use the framework to design development tools capable of compensating for human memory limitations. For developers, the insights and strategies from the framework should allow reflection on our own programming habits and work practices and how they may be tailored to better fit our human brain. Finally, I describe some initial results in using fMRI and EMG to further understand the programmer's brain, with long-term impact in education, evaluation, and tool and language design

Time and place:
10:30am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Thursday, January 16, 2014

11:00am Meeting room 202 (Mountain View), level 2

Laura Titolo, PhD Student, University of Udine, Italy

### An Abstract Interpretation Framework for Diagnosis and Verification of Timed Concurrent Constraint Languages

#### Abstract:

Formal verification of concurrent and reactive systems is necessary for many modern critical applications.
The Timed Concurrent Constraint Language (tccp in short) is a simple but powerful model for concurrent and reactive systems. In this language the notion of time is modeled by a global and discrete clock and the information on system variables is handled by an underlying constraint system.
The existing formal techniques for the verification of tccp are based on model checking, which suffers the well known state-explosion problem.
Abstract interpretation is an alternative to model checking: it is a theory of sound semantic approximation proposed with the aim of providing a general framework for analysis, verification and debugging of systems.
In this talk, I present a semantic framework for tccp based on abstract interpretation with the purpose of formally verifying and debugging tccp programs.
The key point for the efficacy of the proposed methodology is the adequacy of the underlying concrete semantics which models precisely the small-step behavior of tccp and is suitable to be used in the abstract interpretation framework.
The main idea behind my approach is to approximate this concrete semantics into suitable abstract domains in order to obtain effectiveness and efficiency at the price of losing some precision in the results.
More specifically, I present two different abstract domains: the first one approximates the information content of tccp behavioral traces, while the second one approximates the small-step semantics with temporal logic formulas.

Time and place:
11:00am Meeting room 202 (Mountain View), level 2
IMDEA Software Institute, Campus de Montegancedo

### Tuesday, January 14, 2014

11:00am Meeting room 302 (Mountain View), level 3

Giovanni Bernardi, Research Fellow, Trinity College, Dublin, Ireland

### Using higher-order contracts to model session types

#### Abstract:

Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed to properly structure delegation of responsibility between processes.
In this talk we show that a sublanguage of higher-order web-service contracts provides a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in that the meaning of a contract is the set of contracts with which it complies. The proof of full-abstraction depends on the novel notion of complement of a contract. We show that the new notion lets us type more well-formed programs than the commonly used type duality does, thereby improving existing type systems.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo

### Friday, January 10, 2014

11:00am Meeting room 302 (Mountain View), level 3

### Bayesian inference to evaluate information leakage in complex scenarios

#### Abstract:

In this talk we explore the suitability of Bayesian Inference techniques, specifically Markov Chain Monte Carlo methods, to evaluate information leakage in complex scenarios. Using anonymity systems, in particular mix networks, as case study we show that casting problems in the context of Bayesian inference provides an appropriate framework to evaluate security properties (e.g., traceability of messages) in presence of complex constraints. We present a generative probabilistic model of mix network architectures that incorporates a number of attack techniques in the literature that exploit different constrants. We use the model to build a Markov Chain Monte Carlo inference engine based on the Metropolis-Hastings algorithm that calculates the probabilities of who is talking to whom given an observation of the anonymity network. Finally, we briefly overview other Bayesian techniques useful to tackle other security problems, such as Gibbs sampling suitable for user profiling, or particle filtering that allows to consider dynamic behaviour.

Time and place:
11:00am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo