POST-GRADUATE INTENSIVE COURSE ON FORMAL VERIFICATION FOR SECURITY AND PRIVACY, BRAGA, 24-26 MAY 2017
Many privacy and security properties are relational, in the sense that they relate two executions of a system, or the execution of an ideal system, which is secure by assumption, and a real system, for which security is sought. As a consequence, relational properties are an important target for program verification.
The first part of the course will consider relational verification of imperative programs. It will present methods based on product programs and relational program logics, and demonstrate how such methods can be used for information-flow analysis, analysis of timing side-channels, and other relational properties.
The second part of the course will consider the case of probabilistic programs. It will introduce the idea of probabilistic coupling, that is used in the analysis of Markov chains, and demonstrate that many properties of interest are modelled by probabilistic couplings or their generalization. Then, it will develop program logics for proving such properties, and demonstrate its applications to differential power analysis, differential privacy, and provable security.
SUMMER SCHOOL IN PROBABILISTIC PROGRAMMING, BRAGA, SOUTELO, MAY 29TH - JUNE 4TH 2017.
The School is jointly organized by the PT-FLAD Chair and a number of international associations EATCS, ETAPS, ACM SIGLOG, and ACM SIGPLAN.
Probabilistic programming languages are used for modelling and analysis purposes across multiple areas of computer science, including machine learning, security, and quantitative biology. In particular, they provide a rigorous foundation for machine learning where they are used to describe probabilistic models and to perform inference in presence of uncertain information. Probabilistic programs are also used in cryptography and in privacy for modelling and quantifying security.
The goal of the school is to introduce attendants to theoretical and practical aspects of programming languages, and will propose courses that cover the following topics: semantics, analysis, verification, applications to machine learning, privacy, and security. The school will have lectures by Andy Gordon, Catuscia Palamidessi, Christel Baier, Dexter Kozen, Frank Wood, Hongseok Yang, Javier Esparza, Michael Carbin, Peter Selinger, Prakash Panangaden, Sriram Sankaranarayanan, and Vitaly Shmatikov.