**Alessandro Orso***, Professor, Georgia Institute of Technology, USA*

**Abstract:**

Software debugging, which involves localizing, understanding, and removing the cause of a failure, is a notoriously difficult, extremely time consuming, and human-intensive activity. For this reason, researchers have invested a great deal of effort in developing automated techniques and tools for supporting various debugging tasks. Although potentially useful, most of these techniques have yet to fully demonstrate their practical effectiveness. Moreover, many current debugging approaches suffer from some common limitations and rely on several strong assumptions on both the characteristics of the code being debugged and how developers behave when debugging such code. This talk will provide an overview of the state of the art in the broader area of software debugging, discuss strengths and weaknesses of the main existing debugging techniques, present a set of open challenges in this area, and sketch future research directions that may help address these challenges.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

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

**Abstract:**

Many tools, methods and models are available today to manage distributed applications in the Cloud. Aeolus brings a new perspective to automation in this framework: based on a simple, yet expressive component model, it is developing a configuration engine that automatically synthesises a distributed application satisfying high level architectural constraints and specific user requirements. In this talk we will provide an overview of the Aeolus approach and of the associated tools.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Cesare Tinelli***, Professor, The University of Iowa, USA*

**Abstract:**

The field of model checking owes much of its great success and impact
to the use of symbolic techniques to reason efficiently about
functional properties of hardware or software systems. Traditionally,
these techniques have relied on propositional encodings of transition
systems and on propositional reasoning engines such as binary decision
diagrams and SAT solvers. More recently, a number of these techniques
have been adapted, and new ones have been devised, based instead on
encodings into fragments of first-order logic supported by
Satisfiability Modulo Theories (SMT) solvers. These are highly
efficient solvers specialized on checking the satisfiability of
formulas in certain logical theories such as the theory of linear
arithmetic, bit-vectors, arrays, algebraic data types, and so on.
SMT-based model checking methods blur the line between traditional
(propositional) model checking and traditional (first or higher order)
deductive verification. More crucially, they combine the best features
of both by offering the scalability and scope of deductive
verification while maintaining comparable levels of automations as
propositional model checking.

This talk will briefly introduce SMT and then give an overview of
SMT-based model checking, focusing on a number of notable approaches
and techniques.

**Time and place:**

11:00am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Gopal Gupta***, Professor, The University of Texas at Dallas, USA*

**Abstract:**

Coinduction is a powerful technique for reasoning about unbounded sets, unbounded structures, infinite automata, and interactive computations. Where induction corresponds to least fixed points semantics, coinduction corresponds to greatest fixed point semantics. In this talk I will give a tutorial introduction to coinduction and show how coinduction can be elegantly incorporated into logic programming to obtain the coinductive logic programming (co-LP) paradigm. I will also discuss how co-LP can be elegantly used for sophisticated applications that include (i) model checking and verification, including of hybrid/cyber-physical systems (ii) planning and goal-directed execution of answer set programs that perform non-monotonic reasoning.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Neng-Fa Zhou***, Professor, The City University of New York*

**Abstract:**

This talk will give the design principles of the Picat language, highlight the high-level and intuitive abstractions provided by Picat for easy programming, and contemplate why Picat is more robust and scalable than Prolog and could be more accessible than Prolog to ordinary programmers for scripting and modeling tasks.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Michael Emmi***, Post-doctoral Researcher, LIAFA, Université Paris Diderot*

**Abstract:**

The widespread rigorous construction of concurrent software (e.g., reactive event-driven code, high-performance parallel code, and geographically distributed code) hinges on the development of effective programming abstractions, the sound construction of the systems ensuring such abstractions, and automated program analyses. My research investigates the specification of such abstractions (e.g., atomicity specifications such as serializability and linearizability), the formal modeling of computing platforms, including the exploitation of such programming abstractions, and the pertinent program analysis problems (e.g., whether a given implementation meets its specification on a given platform). Besides studying the decidability and complexity of such analysis problems, we develop problem approximations which yield more-tractable algorithms for those highly intractable problems.

In one recent work, we have studied the so-called "explicitly-parallel" programming languages developed for high-performance parallel computing. We have proposed a general formal model of isolated recursive parallel computations, and identified several fragments to match the features present in real-world programming languages such as Cilk and X10. By associating fundamental formal models (vector addition systems with recursive transitions) to each fragment, we provide a common platform for exposing the relative difficulties of algorithmic reasoning. For each case we measure the complexity of deciding state-reachability for finite-data recursive programs, and propose algorithms for the decidable cases. The complexities which include PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable state-reachability for finite-data recursive multi-threaded programs, thus exploiting the additional computational structure imposed by these programming languages.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Tudor Dumitras***, , Symantec Research Labs (SRL)*

**Abstract:**

Because computer systems operate in an ecosystem of users, attackers and inter-dependent software, their security depends on factors that are often specific to the deployment environments. Many security technologies are based on long-held assumptions about these factors. For example, we assume that software systems inevitably include security vulnerabilities, which may be exploited by cyber attackers, and that we can patch the vulnerable hosts before these attacks occur. However, we do not know which vulnerabilities are ultimately exploited in the field and for how long the end-hosts are susceptible to these exploits. To improve the security of systems in active use, we must understand the factors that drive the failures and vulnerabilities of software in the field.

In this talk, I will present two empirical studies that provide fresh insights into these problems and that suggest new opportunities for improving system security. The first study shows that zero-day attacks, which exploit vulnerabilities before their public disclosure, go on undetected for 312 days (approximately 10 months) on average. The duration of zero-day attacks had remained an open question for more than a decade because, in general, data is not collected until after the attack is discovered and because zero-day attacks are rare events that are unlikely to be observed in honeypots or in lab experiments. Additionally, I show that zero-day attacks are more common than previously though: 60% of the vulnerabilities identified in the study were not known to have been used in zero-day attacks. The second study shows that the fraction of vulnerabilities that are actually exploited in the field has been steadily decreasing over the past ten years. Moreover, alternative approaches to patching vulnerabilities, such as attack-surface reduction, have limited effectiveness because attack surfaces vary from one host to another and they cannot be reduced indefinitely without rendering the hosts inoperable.

These results derive from field data collected on 11 million hosts over a period of 3 years. I will also describe the Worldwide Intelligence Network Environment (WINE), the data analytics platform that enabled these studies. By sampling and aggregating up to 19 billion telemetry reports per day, WINE provides representative data for analyzing the past and present cyber-threat landscapes. WINE also allows security researchers to conduct experiments at scale and archives the raw data used in each experiment, for reproducibility.

The empirical results from WINE suggest that we must rethink our current security models, which guide public policy and the design of security technologies. For example, we should focus on accelerating the deployment of security patches (and not just their creation) through efficient mechanisms for online software upgrade. Additionally, these results illustrate the opportunities for improving system security in actively used systems by creating Internet-wide models, derived empirically and updated frequently, for the failures and vulnerabilities of software in the field.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Philipp Leitner***, Post-doctoral Researcher, Vienna University of Technology, Austria*

**Abstract:**

Cloud Computing is one of the most notorious hypes in today's Web information systems research and practice. In this talk, I introduce the basic notions and challenges associated with Cloud Computing, and position my own research agenda within the larger cloud computing, services and software engineering communities. Furthermore, I provide an in-depth look under the hood of CloudScale. CloudScale is an experimental middleware for deploying applications in the Infrastructure-as-a-Service cloud, which we have devised at Vienna University of Technology. I explain how to build applications based on CloudScale, and how such systems can scale up and down via automated resource provisioning. I detail the practical advantages that the CloudScale model offers over competing paradigms. Finally, I conclude the talk with an outlook on current research issues in Cloud Computing, both, within and outside of the CloudScale system.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Jorge A. Navas***, Post-doctoral Researcher, The University of Melbourne, Australia*

**Abstract:**

We present a decision procedure for the problem of, given a set of regular expressions R1,..Rn, determining whether their intersection R = R1 \cap ... \cap Rn is empty. While this problem is decidable, the implementation of pratical algorithms is still an open issue. Current solutions rely on the classical product algorithm for intersection of DFAs (Deterministic Finite Automata). Our solver, Revenant, finitely unrolls the automata from the regular expressions, encoding each as a set of propositional constraints. If a SAT solver determines satisfiability then R is non-empty. Otherwise our solver uses unbounded model checking techniques to extract an interpolant from the bounded proof. This interpolant serves as an overapproximation of R. If the solver reaches a fixed-point with the constraints remaining unsatisfiable, it has proven R to be empty. Otherwise, it increases the unrolling depth and repeats. We compare Revenant with other state-of-the-art string solvers. Evaluation suggests that it behaves better for constraints that express the intersection of sets of regular languages, a case of interest in the context of verification.

This work will be presented at TACAS'13 and it is done together with Graeme Gange, Harald Sondergaard, Peter Schachte and Peter J. Stuckey from the University of Melbourne.

**Time and place:**

11:00am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Johannes Kinder***, Post-doctoral Researcher, EPFL, Switzerland*

**Abstract:**

The amount of software keeps growing steadily, and users are faced with an increasingly complex choice of which applications to trust and install. Existing mechanisms to weed out malicious and bogus apps have so far been insufficient at protecting users.

In my talk, I propose to use program analysis for judging the possible behavior of software. In this setting, one faces potentially malicious developers and cannot rely on their cooperation. Therefore, I apply static analysis directly to binaries and harden it against common obfuscation schemes by tightly integrating it with disassembly and control flow reconstruction. Based on this approach, I show how to statically defeat the infamous "virtualization obfuscation", which compiles programs into bytecode for randomized architectures.

For a complementing dynamic approach, I turn to symbolic execution. I explain tradeoffs in this generally expensive technique and introduce a heuristic for minimizing its cumulative cost, which allows experimental speed-ups of up to ten orders of magnitude.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Ivan Beschastnikh***, PhD Student, University of Washington, USA*

**Abstract:**

Logged messages are invaluable for debugging and diagnosing problems. Unfortunately, many execution logs are inscrutable in their raw form. For example, a production Google system may generate a billion-line log file in a single day. In my talk, I will detail two log-analysis tools that I developed to deal with this problem. These tools infer concise and precise models from large execution logs of sequential and distributed systems. Both tools enable new kinds of program analyses and make logs more useful to developers. For example, my empirical experiments show that developers find the inferred models useful for identifying bugs, confirming bugs that were previously known, and increasing their confidence in their implementations.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Radu Iosif***, Researcher, VERIMAG/CNRS, Grenoble, France*

**Abstract:**

Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments between such formulae are decidable for validity. These predicates are general enough to define (doubly-) linked lists, trees, and structures more general than trees, such as trees whose leaves are chained in a list. The decidability proofs are by reduction to decidability of Monadic Second Order Logic on graphs with bounded tree width.

**Time and place:**

11:00am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Anthony W. Lin***, Post-doctoral Researcher, U. of Oxford*

**Abstract:**

Automatic analysis of integer-manipulating programs is a main problem in program analysis. Such programs are a basic building block of more complex imperative programs (e.g. with linked lists or strings) since analysis of the latter can often be reduced to analysis of the former (e.g. by some variants of counter abstractions). Since they are already Turing-complete, the challenge is to devise approximation techniques that give useful answers in many cases. Following a standard automata-theoretic approach, we will consider Minsky's counter systems as an abstraction of integer-manipulating programs, i.e., finite-state automata with integer counters whose values can be incremented/decremented by and compared against integer constants. In order to analyze such systems, we will consider reversal-bounded acceleration, which is an underapproximation technique that covers runs of a fixed number of reversals between non-incrementing/non-decrementing modes of the counters. We will show that reversal-bounded analysis of counter systems is efficiently reducible to satisfiability of quantifier-free Presburger formulas (in fact, NP-complete) and so can be solved using highly-optimized SMT solvers like Z3. We have implemented a prototype of the reduction and shows the efficacies of the technique on a few interesting examples (e.g. derived from Linux device drivers) which other techniques (e.g. predicate abstractions and bounded-model checking) cannot deal with. This is a joint work with Matthew Hague, which has appeared in CAV'11 and CAV'12.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Dario Fiore***, Post-doctoral Researcher, Max Planck Institute for Software Systems, Germany*

**Abstract:**

In the last thirty years cryptographic research laid the foundations for facing security problems whose solutions impact our daily life. A prominent example of the high influence of this research is the possibility of achieving secure connections in the Internet using SSL or IPSEC.

The IT field, however, rapidly evolves and poses new security challenges in which traditional cryptographic tools (such as public key encryption and digital signatures) do not properly fit. Notably, we witness the rise of cloud computing, a paradigm in which clients or businesses lease computing and storage services from powerful entities usually referred to as "cloud providers". While cloud computing is predicted to be "the future", many security questions are still left unanswered: how to ensure that the cloud computes what it should? How to guarantee the confidentiality of the outsourced data?

Motivated by these questions, I will discuss recent advances in the design of cryptographic primitives that will help securing cloud computing. More specifically, I will focus on the problem of delegating computations on outsourced data. At a high level, this problem involves a client who outsources its data to the cloud, and later wants to delegate computations on such data while being able to verify the correctness of the result. I will show how standard primitives such as digital signatures and message authentication codes fall short of the requirements of this setting. Nevertheless, I will describe how homomorphic versions of these cryptographic tools can elegantly solve the problem. I will then present the notions of homomorphic digital signature and message authentication, and will finally discuss their efficient realizations as well as future challenges in this area.

During the presentation I will also highlight how the interplay of foundational research and practical applications has a significant role in this research activity.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Andrea Cerone***, PhD Student, Trinity College, Dublin, Ireland*

**Abstract:**

We present a process calculus for modelling wireless networks at the Network Layer of the ISO/OSI reference model, that is where point-to-point reliable broadcast is the only communication mechanism between stations.

We introduce a theory of composition of networks, which is used as a basis for developing behavioural preorders in the style of Hennessy and de Nicola. We also provide sound and complete proof techniques for showing whether two networks are related according to one of such preorders.

Finally, we show the usefulness of our proof techniques by verifying the correct behaviour of a routing protocol with respect to a formal specification.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

**Aleksandar Dimovski***, PhD Student, FON University, Macedonia*

**Abstract:**

Game semantics is a denotational semantics which constructs models of terms (open programs) by looking at the ways in which a term can observably interact with its environment. The obtained models are fully abstract (sound and complete), and are the most accurate models we can find for a programming language. Game semantics models can be given certain kinds of concrete automata-theoretic representations for several interesting language fragments with finite data types, and so they can serve as a basis for software model checking and program analysis. Here we examine several techniques for automatic verification of safety properties of terms with infinite data types.

We have developed an abstraction-refinement procedure, which starts by model-checking the most abstract version of the concrete program. If no counterexample or a genuine one is found, the procedure terminates. Otherwise, it uses a spurious counterexample to gradually refine the abstraction for the next iteration.

We can combine this approach with a method for verifying data-independent terms. We say that a term is data-independent with respect to a data type X, if the only operation available on values of type X is the equality test. We provide results which reduce the verification of some properties for all interpretations of X, to the verification for finite interpretations of X.

Finally, we present a new symbolic approach for representing game semantics models, and show how it can be applied for efficient verification of terms. By using symbolic values instead of concrete ones, we generalize the standard notion of automata representation of game semantics to that of symbolic-automata representation. In this way terms with infinite data types can be expressed as finite-state symbolic-automata, and so various properties can be checked over them.

**Time and place:**

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

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain