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

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