Palestrante convidada: Catuscia Palamidessi (INRIA Saclay, França)

Biografia resumida: Catuscia Palamidessi é Diretora de Pesquisa da INRIA Saclay, onde lidera a equipe COMETE. Ela obteve seu título de PhD na Universidade de Pisa em 1988. Veja mais detalhes...

Data: segunda-feira (26-set-2011)
Horário: 16:30 - 18:00

Resumo (inglês): 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.

Palestrante convidado: John Harrison (Intel Corporation, EUA)

Biografia resumida: John Harrison realiza verificação formal na Intel Corporation. Ele se especializou principalmente em verificação de algoritmos de ponto flutuante e de outros softwares matemáticos, mas ele se interessa por todos os aspectos de prova e verificação de teoremas. Veja mais detalhes...

Data: terça-feira (27-set-2011)
Horário: 9:00 - 10:30

Resumo (inglês): 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.