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

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