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