Talk title: Quantitative Information Flow and Relation with Differential Privacy

Short bio: Catuscia Palamidessi is Director of Research at INRIA Saclay, where she leads the team COMETE. She got her PhD at the University of Pisa in 1988. See more details...

Date: Monday (Sep 26, 2011)
Time: 16:30 - 18:00

Abstract: One of the concerns in the use of computer systems is to avoid the leakage of secret information through public outputs. Ideally we would like systems to be completely secure, but in practice this goal is often impossible to achieve. Therefore it is important to have a way to assess the amount of leakage. In this talk, we illustrate the information-theoretic approach to measure the leakage, and various scenarios depending on the model of adversary. We also make a connection with the recent notion of "differential privacy" which is another way to quantify information leakage, developed independently in the area of statistical databases.

Talk title: Formal Methods at Intel - An Overview

Short bio: John Harrison does formal verification at Intel Corporation. He has mainly specialized in verification of floating-point algorithms and other mathematical software, but he is interested in all aspects of theorem proving and verification. See more details...

Date: Tuesday (Sep 27, 2011)
Time: 9:00 - 10:30

Abstract: Since the 1990s, Intel has invested heavily in formal methods, which are now deployed in several domains: hardware, software, firmware, protocols etc. Many different formal methods tools and techniques are in active use, including symbolic trajectory evaluation, temporal logic model checking, SMT-style combined decision procedures, and interactive higher-order logic theorem proving. I will try to give a broad overview of some of the formal methods activities taking place at Intel, and describe the challenges of extending formal verification to new areas and of effectively using multiple formal techniques in combination.