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