IMDEA initiative
Abstract: Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful compu...
Abstract: In this talk I will present two algorithmical approaches to static partial order reduction for Markov Decision Processes...
Abstract: Test Data Generation aims at automatically obtaining test inputs that can be used to validate the functional behaviour o...
Abstract: We describe semi-automatic verification of the software barrier synchronization primitive. We improve the state of the a...
Abstract: Hoare Type Theory (HTT) is as a powerful tool for "structuring the verification of heap manipulating programs"
Abstract: Java monitors as implemented in the java.util.concurrent.locks package provide no-priority nonblocking monitors. That is...
Abstract: I will be giving an informal presentation of results from a recently concluded study on the heap structures that appear ...
Abstract: Specifications of concurrent libraries are commonly given by the well-known notion of linearizability. However, to date ...
Abstract: Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of pop...
Abstract: There are two active and independent lines of research that aim at quantifying the amount of information that is reveale...
Abstract: Linear logic Concurrent Constraint programming (LCC) is an extension of concurrent constraint programming (CC) where the...
Abstract: We present a framework for (static) verification of general resource usage program properties. The framework extends the...
Abstract: In Service-Oritented Computing, business processes are usually expressed in terms of workflows that describe control and...
Abstract: Theorem provers based on dependent types rely on efficient full-reducers implementing a beta-equivalence tester for thei...
Abstract: In multi-threaded programs data is often separated into lock-protected resources. Properties of those resources are typi...
Abstract: This talk presents Relational Hoare Type Theory (RHTT), a language and verification system for expressing and verifying ...
Abstract: In functional programming one usually writes programs as the composition of simpler functions. Consequently, the result ...
Abstract: Coding rules are used in industry to enforce good software practices that improve software reliability and maintainabili...
Abstract: We investigate the issue of determining whether the intersection of a context-free language (CFL) and a Petri net langua...
Abstract: The automata-theoretic approach to model checking reduces a model checking problem to automata constructions and automat...
Abstract: A security analyst often needs to understand two runs of the same program that exhibit a difference in program state or ...
Abstract: We present a declarative language with a formal semantics for specifying both users’ privacy preferences and servi...
Abstract: Recent progress in solvers modulo theories reach a point where it seems feasible to perform automatic static analysis of...
Abstract: Modern concurrency logics are sound only with respect to the interleaving semantics, which assumes scheduling is impleme...
Abstract: The analysis of code that uses cryptographic primitives is unfeasible with current state-of-the-art symbolic execution t...
Abstract: Reachability of a program location in the concurrent program is an undecidable problem. The pattern based verification i...
