IMDEA initiative
Abstract: Aggregates are used to compute single pieces of information from separate data items, such as records in a database or a...
Abstract: Some of the recent blockchain proposals, such as Stellar and Ripple, use quorum-like structures typical for Byzantine co...
Abstract: Modern cryptography is a pessimistic discipline, in at least two ways: pessimistic in its fundamental belief (“The...
Abstract: In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed...
Abstract: Mixing Networks are protocols that allow a set of senders to send messages anonymously. Such protocols are fundamental b...
Abstract: Almost every programming language possess some kind of type system. These systems ensures some safety over the code exec...
Abstract: Today’s workloads in the datacenter suffer from stagnating CPU performance and increasing data volumes. One promis...
Abstract: The Transport Layer Security (TLS) protocol is the de-facto standard for encrypted communication on the Internet. Howeve...
Abstract: Symmetric key cryptography is an essential part of communication systems, where a secret key is used to protect data con...
Abstract: The Knaster-Tarski Lemma is one of the main tools for obtaining fixpoints. There are also iterative methods, and these a...
Abstract: Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward...
Abstract: Stream Runtime Verification (SRV) is a behavioral specification language for runtime verification, where a monitor is de...
Abstract: Stream Runtime Verification (SRV) is a specification formalism for temporal properties of reactive systems where observa...
Abstract: Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis sound...
Abstract: A program that computes on an infinite data structure, such as an infinite list or tree cannot be expected to terminate....
Abstract: Prime numbers are essential in cryptography. Many cryptographic primitives (RSA encryption, ElGamal, digital signatures...) rely on finding and using...
Abstract: Many micro-architectural attacks rely on the capability of an attacker to efficiently find small eviction sets: groups o...
Abstract: We extend the simply-typed guarded λ-calculus with discrete probabilities and endow it with a program logic for reasonin...
Abstract: The celebrated Parikh’s Theorem states that every context-free language is equivalent to a regular language when w...
Abstract: Modern computer architectures rely on caches to reduce the latency gap between the CPU and main memory. While indispensa...
Abstract: Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate cer...
Abstract: It is expected that nonvolatile, byte-addressable memory (NVM) will soon be commonplace. However, registers and caches a...
Abstract: Cross-Site Request Forgery (CSRF) attacks are one of the critical threats to web applications. In a CSRF attack, an atta...
Abstract: Facebook, Google, Amazon and many other large companies produce huge amounts of data that they need to store and process...