IMDEA initiative
Abstract: Vague or “fuzzy” concepts appear almost everywhere. The combination of fuzzy logic with logic programming op...
Abstract: We present a declarative language with a formal semantics for specifying both users’ privacy preferences and servi...
Abstract: Contents: We give a short survey on the following topics on verification of multithreaded programs: SPIN Specification i...
Abstract: The notion of approximate equivalence of programs plays a fundamental role in several fields of computer science. In par...
Abstract: Zero-knowledge proofs are two-party interactive protocols where one party (the prover) convinces the other one (the veri...
Abstract: Relational program logics allow reasoning about two programs or two runs of the same program. They provide an elegant me...
Abstract: In this talk we present a MySQL code generator for OCL expressions which is based on the use of stored procedures for ma...
Abstract: Implementors of abstract machines face complex, and often interacting, decisions regarding, e.g., data representation, i...
Abstract: “Shared resources” is the term we use to refer to the notation and companion methodology used to teach concu...
Abstract: Side-channel attacks break cryptosystems by exploiting information that is revealed by the system’s implementation...
Abstract: I introduce subsequence invariants, a new class of invariants for the specification and verification of concurrent syste...
Abstract: Separating data into lock-protected resources is an established paradigm of multi-threaded programming. Programs followi...
Abstract: Pure lambda calculus reduction strategies have been thoroughly studied, as they constitute the foundations of evaluation...
Abstract: Glass-box test data generation (TDG) is the process of automatically generating test input data for a program by conside...
Abstract: We consider the refinement of a static analysis method called thread-modular verification. It was an open question wheth...
Abstract: We present a development environment for automatically building smart, security-aware GUIs following a model-based appro...
Abstract: We apply the framework of abstract interpretation to derive an abstract semantic function for the modal μ-calculus. The ...
Abstract: Non-failure analysis aims at inferring that procedure calls in a program will never fail. This type of information has m...
Abstract: Constraint Handling Rules (CHR) is a concurrent committed-choice rule-based programming language introduced in the 1990s...
Abstract: Cryptography is decidable
Abstract: Formal verification of imperative programs provides a high guarantee of software reliability, but it is usually a human ...
Abstract: Service compositions define how serveral Web services (loosely coupled platform independent software components exposed ...
Abstract: Model-checking techniques suffer from the state explosion problem that prevents them to scale up. During the past decade...
Abstract: A difficult point when verifying heap manipulating programs is to be able to separate precisely the part of the heap tha...
Abstract: Regular Linear Temporal Logic (RLTL) is a temporal logic that extends the expressive power of Linear Temporal Logic (LTL...
Abstract: This is a followup to my previous talk on the topic. where I presented the basics of abstract interpretation and of para...
Abstract: Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as f...
Abstract: Shared mutable objects pose challenges in reasoning, especially for data abstraction and modularity. We present a logic ...
Abstract: What to do when we have an empty slot in our popular Theory lunch series? Respond to the overwhelming popular demand for...
