Nazareno Aguirre

Thursday, December 19, 2019

Nazareno Aguirre, Associate Research Professor, Universidad Nacional de Río IV, Argentina

Tight Bounds and Applications in Generalized Symbolic Execution and Test Input Generation

Abstract: It is well known that various scalability issues affect automated formal verification, and thus some approaches need to ...


Abstract: CAPTCHA systems have been widely deployed to identify and block fraudulent bot traffic. However, current solutions, such...


Abstract: Embedded software plays a steadily increasing role in all industrial sectors, and in several such sectors software is re...


Jan Tretmans

Monday, November 25, 2019

Jan Tretmans, Associate Research Professor, Radboud University, Netherlands

Goodbye ioco, hello uioco

Abstract: Model-based testing (MBT) is a systematic way of black-box testing of a system under test (SUT) with respect to behaviou...


Giovanni Denaro

Friday, November 22, 2019

Giovanni Denaro, Associate Research Professor, University of Milano-Bicocca, Italy

Automatic Test Generation for Programs with Complex Structured Inputs

Abstract: Despite the recent improvements in automatic test case generation, test case generators do not yet handle well programs ...


Ignacio Luengo

Monday, November 18, 2019

Ignacio Luengo, Professor, Universidad Complutense de Madrid, Spain

Post-quantum Cryptography with polynomials

Abstract: Post-quantum cryptography is public-key cryptography resistant to future quantum computers. In this talk we will talk ab...


Veronica Dahl

Monday, November 4, 2019

Veronica Dahl, Research Professor, Simon Fraser University, Canada

AI for Social Responsibility: Embedding principled guidelines into AI systems

Abstract: In this position talk we briefly retrace the historic and evolutionary context that led to AI’s results not necess...


Bernardo David

Wednesday, October 16, 2019

Bernardo David, Associate Research Professor, IT University of Copenhagen, Denmark

Efficient Privacy Preserving Computation meets Blockchains

Abstract: Multiparty Computation (MPC) protocols allow a set of mutually distrustful parties to compute a program without revealin...


Yu-yang Lin

Tuesday, October 15, 2019

Yu-yang Lin, PhD Student, Queen Mary, London University

A Bounded Model Checking Technique for Higher-Order Programs

Abstract: We present a Bounded Model Checking technique for higher-order programs based on defunctionalization and points-to analy...


Alejandro Ranchal-Pedrosa

Monday, October 14, 2019

Alejandro Ranchal-Pedrosa, PhD Student, University of Sydney, Australia

Platypus: Offchain Protocols without Synchrony

Abstract: Offchain protocols aim at bypassing the scalability and privacy limitations of classic blockchains by allowing a subset ...


Christian Roldán

Wednesday, October 2, 2019

Christian Roldán, PhD Student, University of Buenos Aires, Argentina

About semantics of replicated data stores

Abstract: Replicated data stores provide highly available, low-latency access to data at the expense of consistency, i.e., observe...


Gregory Chockler

Tuesday, September 10, 2019

Gregory Chockler, Research Professor, Royal Holloway, University of London, United Kingdom

Atomic Transaction Commit for Modern Data Stores

Abstract: Transaction commit protocols play a pivotal role in supporting scalability and availability guarantees of today’s ...


Yotam Feldman

Wednesday, September 4, 2019

Yotam Feldman, PhD Student, Tel Aviv University, Israel

Inferring Inductive Invariants from Phase Structures

Abstract: Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or auto...


Yotam Feldman

Tuesday, September 3, 2019

Yotam Feldman, PhD Student, Tel Aviv University, Israel

Order out of Chaos: Proving Linearizability Using Local Views

Abstract: Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is...


Antonio Nappa

Tuesday, July 2, 2019

Antonio Nappa, Researcher, Brave Software

Trusted Hardware: The Good, The Bad, The Ugly

Abstract: Trusted hardware is one of the most complex and desired components of modern computers. For example, almost all mobile p...


Mooly Sagiv

Wednesday, June 12, 2019

Mooly Sagiv, Research Professor, Tel Aviv University, Israel

Deductive verification of distributed protocols in first-order logic

Abstract: Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed p...


František Farka

Tuesday, April 30, 2019

František Farka, PhD Student, Heriot-Watt University, United Kingdom

Proof-Relevant Resolution: The Foundations of Constructive Automation

Abstract: In this talk, we introduce proof-relevant resolution, a framework for constructive proof automation. The intended applic...


Ignacio Cascudo

Friday, April 26, 2019

Ignacio Cascudo, Assistant Research Professor, Aalborg University, Denmark

Some developments in secure multiparty computation for binary circuits

Abstract: Secure multiparty computation studies deals with privacy-preserving computation, where several parties, some of them hol...


Abstract: In this talk, I will present pretend synchrony, a new approach to verifying distributed systems, based on the observatio...


Marco Guarnieri

Wednesday, April 24, 2019

Marco Guarnieri, Post-doctoral Researcher, IMDEA Software Institute

Principled detection of speculative information flows

Abstract: Modern CPUs employ speculative execution to avoid expensive pipeline stalls by predicting the outcome of branching (and ...


Joao Marques Silva

Tuesday, April 23, 2019

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 explanat...


Abstract: Many artifacts that software developers produce are written in natural language: code comments, commit messages, text in...


Maria Schett

Wednesday, April 10, 2019

Maria Schett, PhD Student, University College London, United Kingdom

Blockchain Superoptimizer

Abstract: Etherum smart contracts written in higher level programming languages like Solidity or Viper are compiled to bytecode, w...


Kenji Maillard

Wednesday, April 10, 2019

Kenji Maillard, PhD Student, INRIA Paris, France

Designing Dijkstra Monads

Abstract: Verifying a program consist of proving that a given program meets its specification. Various frameworks have been studie...


Abstract: Fabric is a modular and extensible open-source system for deploying and operating permissioned blockchains and one of th...


Ingo Mueller

Friday, April 5, 2019

Ingo Mueller, Post-doctoral Researcher, ETH Zurich, Switzerland

The State of the Art of Data Analytics Systems and What is Wrong about it

Abstract: Few technological advances have affected as many aspects of science, economy, and society in general as the ability to c...


Joseph Izraelevitz

Thursday, April 4, 2019

Joseph Izraelevitz, Post-doctoral Researcher, UC San Diego

Practical and Formal Infrastructure for Nonvolatile Memory

Abstract: For decades, programmers have interacted with persistent storage via a well-defined block-based API, namely, that of the...


Andreas Pavlogiannis

Tuesday, March 26, 2019

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 ...


Abstract: The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other syst...


Abstract: Security often fails in practice due to a lack of understanding of the nuances in real-world systems. For example, users...


Martin A.T. Handley

Tuesday, March 19, 2019

Martin A.T. Handley, PhD Student, University of Nottingham, United Kingdom

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...


Eduardo Bezerra

Thursday, March 14, 2019

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 th...


Michael D. Adams

Monday, January 21, 2019

Michael D. Adams, Software Engineer, University of Utah, USA

Advances in Parsing

Abstract: Parsing is sometimes thought of as a solved problem. However, recent advances show that there is still much to be discov...


Miguel Á.  Carreira-Perpiñán

Friday, January 18, 2019

Miguel Á. Carreira-Perpiñán, Professor, University of California at 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 i...


Julian Thomé

Friday, January 11, 2019

Julian Thomé, Junior researcher, places.SL

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 detec...