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