IMDEA initiative
Abstract: In this talk I will give an overview of my current research. The focus is on automatic analysis for message passing base...
Abstract: State machine replication (SMR) is a well-established approach to developing highly available services. In essence, the ...
Abstract: The advent of Software-as-a-Service (SaaS) has led to the development of Multi-Party Web Applications (MPWAs). MPWAs rel...
Abstract: Recent developments on SMT solvers have become crucial to make program analysis techniques effective in practice. Despit...
Abstract: Web service operators set up reverse proxies to interpose the com- munication between clients and origin servers for loa...
Abstract: We will review the possible approaches to defining memory models for programming languages, and will describe the C11 me...
Abstract: As a society we have come to rely upon our mobile phones for myriad daily tasks. It is striking how little insight we, a...
Abstract: In large scale distributed systems, strong consistency criteria like sequential consistency and linearizability are ofte...
Abstract: Storage systems based on Weak Consistency provide better availability and lower latency than systems that use Strong Con...
Abstract: As every aspect of our lives gets more dependent on technology and the Internet, it is becoming more necessary to protec...
Abstract: Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective...
Abstract: The C++ relaxed memory model is very challenging. The crucial task of writing correct and efficient low-level concurrent...
Abstract: Type systems are a widely used techniques for programming languages analysis. They are used to avoid undesired behaviour...
Abstract: JavaScript not only makes it easy to write concise code in short time, but also to introduce programming errors, many of...
Abstract: We construct new leakage-resilient signature schemes. Our schemes remain unforgeable against an adversary leaking arbitr...
Abstract: Governments increasingly store and process huge quantities of data to combat crime, fraud, and terrorism with the aim of...
Abstract: Software developers are an ideal channel for the distribution of discrete optimization (DO) technology. Unfortunately, i...
Abstract: The past decade has witnessed a sea change in the perception of formal software verification. For instance, the microker...
Abstract: In recent years, many organizations have established bounty programs that attract white hat hackers who contribute vulne...
Abstract: Porting a software testing execution environment to a cloud-based infrastructure can lead to significant test speedup an...
Abstract: Most definitions of weak consistency models (WCM) in the literature are specific to one style of semantics description (...
Abstract: Consistency is hard and coordination is expensive. As we move into the world of connected “Internet of Things” style app...
Abstract: We revisit the question of constructing an ideal cipher from a random oracle. Coron et al.~(Journal of Cryptology, 2014)...
Abstract: Hard real-time systems require programs to react on time. Static timing analysis derives timing guarantees by analyzing ...
Abstract: The amount and value of information we store in computers, servers or the collective cloud keeps growing while the ways ...
Abstract: By adding redundancy to transmitted data, error-correcting codes(ECCs) make it possible to communicate reliably over noi...
Abstract: Modern replicated data stores aim to provide high availability, by immediately responding to client requests, often by i...
Abstract: Signal Processing has successfully become an instrumental discipline in addressing the challenges posed by the digital w...
Abstract: This talk will present the design and soundness proof of Verasco, a formally verified static analyzer for most of the IS...
Abstract: Security and privacy issues in medical Wireless Body Area Networks (WBANs) constitute a major unsolved concern because o...