IMDEA initiative
Abstract: Internet traffic is exposed to potential eavesdroppers. Standard encryption mechanisms do not provide sufficient protect...
Abstract: Secure multi-execution (SME) is a dynamic technique to ensure secure information flow. In a nutshell, SME enforces secur...
Abstract: Drive-by downloads are the preferred distribution vector for many malware families. In the drive-by ecosystem many explo...
Abstract: RFuzzy framework is a Prolog-based tool for representing and reasoning with fuzzy information. The advantages of our fra...
Abstract: TACO is a tool for formal verification of programs that helps developers find bugs in early stages. TACO translates anno...
Abstract: Security protocols and APIs are difficult to specify and implement. A reference or prototype implementation written in C...
Abstract: Lazy Clause Generation is a powerful approach for reducing search in Constraint Programming. It works by recording the r...
Abstract: Program synthesis offers an effective means to exhaustively explore the design space of a class of algorithms: it can se...
Abstract: Static Cost Analysis aims at estimating the amount of resources that an execution of a given program consumes. By resour...
Abstract: Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goals is to ...
Abstract: Two competing approaches to handling complex constraints in satisfaction and optimization problems using SAT and LCG/SMT...
Abstract: In this talk, I will present our recent study on the decidability of termination of several variants of simple integer l...
Abstract: The evaluation of Prolog, the most successful Logic Programming language, is based on the SLD resolution strategy. SLD p...
Abstract: The notion of "zero-knowledge proof" (an instance of the more general notion of "interactive proof") is an intriguing concept from...
Abstract: Normal order is the standard full-reducing strategy of the pure lambda calculus. It delivers the normal form of a term i...
Abstract: Self-adjusting computation is a language-based approach to writing incremental programs that respond dynamically to inpu...
Abstract: We present an efficient declarative execution mechanism for Logic Programming. Our machine is based on the categorical v...
Abstract: The latency gap between caches and main memory has been successfully exploited for recovering sensitive input to program...
Abstract: From Owicki-Gries’ resource invariants and Jones’ rely/guarantee to modern variants based on separation logi...
Abstract: This poster describes frontiers in verification of the software barrier synchronization primitive. So far most software ...
