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

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