Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas

Charlas Invitadas

Joao Marques Silva

Tuesday, April 23, 2019

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

Joao Marques Silva, Research Professor, Universidade de Lisboa

Logic-Enabled Explanations for Machine Learning Models

Abstract:

The practical successes of Machine Learning (ML) in different settings motivates the ability of computing small explanations for predictions made. Small explanations are generally accepted as easier for human decision makers to understand. Existing work on computing explanations is based on heuristic approaches, providing no guarantees of quality, in terms of how close such solutions are from cardinality- or subset-minimal explanations. This talk describes a novel constraint-agnostic approach for computing explanations for any Machine Learning (ML) model. The proposed solution exploits abductive reasoning, and imposes the requirement that the ML model be represented as sets of constraints using some target constraint reasoning system for which the decision problem can be answered with some oracle. The talk also compares the new logic-enabled approach for computing explanations with existing heuristic approaches on well-known datasets.


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


Marko Vukolić

Monday, April 08, 2019

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

Marko Vukolić, Researcher, IBM Research - Zurich

Hyperledger Fabric: a Distributed Operating System for Permissioned Blockchains

Abstract:

Fabric is a modular and extensible open-source system for deploying and operating permissioned blockchains and one of the Hyperledger projects hosted by the Linux Foundation (www.hyperledger.org). Fabric supports modular consensus protocols, which allows the system to be tailored to particular use cases and trust models. Fabric is also the first blockchain system that runs distributed applications written in standard, general-purpose programming languages, without systemic dependency on a native cryptocurrency. This stands in sharp contrast to existing blockchain platforms that require "smart-contracts" to be written in domain-specific languages or rely on a cryptocurrency. Fabric realizes the permissioned model using a portable notion of membership, which may be integrated with industry-standard identity management. To support such flexibility, Fabric introduces an entirely novel blockchain design and revamps the way blockchains cope with non-determinism, resource exhaustion, and performance attacks. Although not yet performance-optimized, Fabric achieves, in certain popular deployment configurations, end-to-end throughput of more than 3500 transactions per second (of a Bitcoin-inspired digital currency), with sub-second latency, scaling well to over 100 peers. In this talk we discuss Hyperledger Fabric architecture, detailing the rationale behind various design decisions. We also briefly discuss distributed ledger technology (DLT) use cases to which Hyperledger Fabric is relevant, including financial industry, manufacturing industry, supply chain management, government use cases and many more.


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


Andreas Pavlogiannis

Tuesday, March 26, 2019

10:45am Lecture hall 1, level B

Andreas Pavlogiannis, Post-doctoral Researcher, EPFL, Switzerland

Algorithmic Advances in Automated Program Analysis

Abstract:

Modern-day software is increasingly complex and software engineering is commonly accepted as a challenging, error-prone task. Consequently, software bugs are prevalent, incurring detrimental financial costs and often risking human lives. Program analyses provide rigorous and effective means to automated bug detection, and are becoming an integral part of the software development process. In this talk, I will present recent algorithmic advances in two impactful domains of program analysis: (i) static analysis and (ii) stateless model checking. Static analyses are lightweight approximations to program behavior and largely constitute the first step to bug detection in the software development process. In the first part, I will introduce the Algebraic Path Problem on Recursive Graphs (APP) and its close variant of Dyck Reachability (DR). These problems serve as algorithmic formulations of static analyses on various domains, such as dataflow/alias/data-dependence analysis and program slicing. I will present new algorithms for APP and DR based on the graph-theoretic notion of treewidth, that lead to theoretical complexity improvements and provide a significant scalability boost in practice. Stateless model checking is one of the most influential techniques in the analysis of concurrent programs because of its effectiveness in dealing with the state-explosion problem. In the second part, I will present Dynamic Partial Order Reduction (DPOR), a widespread stateless technique for model checking concurrent programs. I will outline some foundational limitations to existing DPOR approaches, and introduce a new abstraction of concurrent semantics, called the Observation Equivalence (OE), which overcomes some of these limitations. I will demonstrate algorithmic applications of OE in two domains: (i) stateless model checking and (ii) dynamic race detection.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Paolo Giarrusso

Friday, March 22, 2019

10:45am Lecture hall 1, level B

Paolo Giarrusso, Post-doctoral Researcher, EPFL, Switzerland

Towards Semantic Type Soundness for Dependent Object Types and Scala with Logical Relations in Iris

Abstract:

The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other systems combining subtyping and forms of dependent types. Soundness of important Scala features remains an open problem in theory and in practice. To obtain a more extensible metatheory, in ongoing work we prove in Coq soundness of DOT semantically. This is challenging, because in DOT variables can be in scope in their own type, objects can define mutually recursive and impredicative type members, and can contain evidence of subtyping relations that must be sound. We address these challenges by novel applications of step-indexing, as supported by the Iris logic. Our proof clarifies difficulties in past proofs; ongoing work on extensions, such as paths, appears encouraging.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Rahul Chatterjee

Thursday, March 21, 2019

10:45am Lecture hall 1, level B

Rahul Chatterjee, PhD Student, Cornell University, New York, USA

Empiricism-Informed Secure System Design: From Improving Passwords to Helping Domestic Violence Victims.

Abstract:

Security often fails in practice due to a lack of understanding of the nuances in real-world systems. For example, users choose weak passwords to deal with the several usability issues with passwords, which in turn degrades the security of passwords. I will talk about how we can build better security mechanisms by combining methodical empiricism with analytical frameworks. First, in the context of passwords, I will show how to improve the usability of passwords by allowing users to log in with typos in their passwords. I will detail in the talk how to do so without giving attackers any additional advantage to impersonate a user. In the second part of my talk, I will talk about my recent research direction on how traditional authentication mechanisms fail to properly model digital attacks by domestic abusers, and therefore are ineffective for victims. As a result, abusers can spy on, stalk, or harass victims using seemingly innocuous apps and technologies. I will finish with some recent progress that I have made in helping victims of tech abuse, and provide some future research directions.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Martin A.T. Handley

Tuesday, March 19, 2019

10:45am Lecture hall 1, level B

Martin A.T. Handley, PhD Student, Universidad de Nottingham, UK

Liquidate your assets: reasoning about resource usage in Liquid Haskell

Abstract:

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this interactive talk, I demonstrate how Liquid Haskell can also be used to reason about program efficiency in the same setting, with the system’s existing verification machinery being used to ensure that the results are both meaningful and precise. My experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and even that the two can coincide. I hope to convince you of the same!


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Eduardo Bezerra

Thursday, March 14, 2019

10:45am Meeting room 202 (Hill View), level 2

Eduardo Bezerra, Software Engineer, Amazon Madrid

Strong Consistency at Scale

Abstract:

Today’s online services must meet strict availability and performance requirements. State machine replication, one of the most fundamental approaches to increasing the availability of services without sacrificing strong consistency, provides configurable availability but limited performance scalability. Scalable State Machine Replication (S-SMR) achieves scalable performance by partitioning the service state and coordinating the ordering and execution of commands. While S-SMR scales the performance of single-partition commands with the number of deployed partitions, it relies on atomic multicast and can present higher latency than traditional SMR, specially when executing multi-partition commands. In this talk, Eduardo Bezerra will revisit Scalable State Machine Replication and Ridge, a high-throughput, low-latency multicast algorithm that mitigates that issue.


Time and place:
10:45am Meeting room 202 (Hill View), level 2
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Michael D. Adams

Monday, January 21, 2019

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

Michael D. Adams, Software Engineer, Universidad de Utah, EE.UU.

Advances in Parsing

Abstract:

Parsing is sometimes thought of as a solved problem. However, recent advances show that there is still much to be discovered in this area. This talk reviews two such advances: indentation-sensitive parsing and disambiguation via tree automata. Several popular languages, such as Haskell, Python, and F#, use the indentation and layout of code as part of their syntax. Parsers for these languages currently use ad hoc techniques to handle layout. This talk presents a simple extension to context-free grammars that can express these layout rules, and derives GLR and LR(k) algorithms for parsing these grammars. Dealing with precedence and associativity rules in context free grammars (CFGs) has long posed a challenge. While they can be encoded in the structure of the CFG, the result can be difficult to work with and often obfuscates the language designer’s intent. This talk shows how tree automata can specify all of these while still allowing the CFG to be written in a natural manner. This unified theory subsumes and generalizes these other techniques and provides an elegant means of specifying grammatical restrictions. These advances indicate that there is still much to be discovered about parsing. We have only uncovered the tip of the iceberg


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


Miguel Á.  Carreira-Perpiñán

Friday, January 18, 2019

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

Miguel Á. Carreira-Perpiñán, Professor, Universidad de California (Merced), USA

A new way to train decision trees: tree alternating optimization (TAO)

Abstract:

Decision trees with hard decision nodes stand apart from other machine learning models in their interpretability, fast inference and automatic feature selection -- in addition to their ability to handle naturally nonlinear data, multiclass classification and regression, discontinuous predictor functions, and discrete input features. This has made decision trees widespread in certain practical applications for decades, in spite of the fact that their predictive accuracy is generally considered inferior to that of other models. In fact, this perceived lower accuracy is greatly due to the lack of a good learning algorithm. Learning a decision tree from data is a difficult optimization problem because of the search over discrete tree structures and the lack of gradient information over the node parameters. The most widespread tree learning algorithms in practice (CART, C4.5 and variations of them) date back to the 1980s and are based on greedily growing the tree structure and setting the node parameters via a heuristic criterion. We present a new algorithm, tree alternating optimization (TAO), that makes it practical for the first time to learn decision trees with a guarantee that the classification error is systematically reduced. Starting with a given tree structure and node parameters, TAO iteratively updates the parameters so that the resulting tree has the same or a smaller structure and provably reduces or leaves unchanged the classification error. TAO can be applied to both axis-aligned and oblique trees and our experiments show it consistently outperforms various other algorithms while being highly scalable to large datasets and trees. Further, TAO can handle a sparsity penalty, so it can learn "sparse oblique trees", having few nonzero parameters at each node. This combines the best of axis-aligned and oblique trees: flexibility to model correlated data, low generalization error, fast inference, smaller trees and interpretable nodes that involve only a few features in their decision. This makes decision trees attractive even in tasks where they were traditionally unsuitable, such as MNIST handwritten digit classification. This is joint work with my PhD students Pooya Tavallali and Arman Zharmagambetov.


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


Julian Thomé

Friday, January 11, 2019

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

Julian Thomé, Junior researcher, ShiftLeft

Automated Security Code Analysis Made Easy

Abstract:

Security auditing, i.e., the examination of the source code for the purpose of detecting vulnerabilities, helps to detect vulnerabilities during the early phases of software development. When performed manually, this task can be laborious, error-prone and does not scale to large software systems. Over the course of the last years, a lot of research has been done with regard to approaches in the areas of Static Analysis, Symbolic Execution and Constraint Solving which aim to make security auditing more effective and cost-efficient. In this presentation, we will see how we at ShiftLeft automate security auditing by using a pragmatic approach, i.e., the combination of techniques proposed by the research community and security expert knowledge, which allows us to support different languages/frameworks and scale to large software systems. We will also see some examples with a live demonstration of our security auditing tool Ocular.


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


Charlas Invitadas - 2018