Page d'accueil // SnT // Distinguishe... // Semantics for noninterference security: Rhyme and Reason - November 17, 2011

Semantics for noninterference security: Rhyme and Reason - November 17, 2011

It is our pleasure to host this distinguished lecture by Prof. Carroll Morgan, University of New South Wales. The lecture will be followed by a reception. Please feel free to forward this invitation

Date: November 17, 2011
Time: 16:30
Venue:  CRP Henri Tudor - Salle Nancy

Abstract: Computer-science style reasoning about programs always benefits from notations that are consistent, that are easy to calculate with, and that avoid where possible a dependence on auxiliary definitions that must be given in some surrounding narrative. We are more interested in dry, systematic prose than in the mathematical poetry of objects that enjoy properties, of facts that are easy to see, and of whences, hences and therefores.

Notations for elementary probability theory seem to respond especially well to a formal-methods motivated reorganisation that recognises the essential role of free- and bound variables, of expressions standing in-line for functions and of step-by-step calculation --- at least when the probabilities are applied to program semantics.

In this talk I will present an alternative notation for elementary probability theory that is principally inspired by computer-science notations already in use elsewhere; and I will give examples of it that are based on well-known probability puzzles.

The talk is stand-alone, and not at all complicated; but its purpose is not to help to solve puzzles. Rather the motivation for paying the cost of using an alternative notation is provided by the afternoon lecture (and other works), where it allows much more succinct and reliable presentation of the essential ideas.

Prof. Carroll Morgan specialises in Formal Methods, particularly program algebras and their supporting semantics. His early contributions were to the theory of program specification and development, the mathematical formulation of Stepwise Refinement, particularly in the context of Abrial's Z (later "B") methods. He has also published on concurrency; and he is the author of the monograph Programming from Specifications.

"Recently" (the last 15 years) he has concentrated on propagating specification/refinement methods to more exotic domains such as probability, and is co-author (with Annabelle McIver) of the resulting monograph Abstraction, Refinement and Proof for Probabilistic Systems. In the last 5 years he has worked on refinement-based approaches to noninterference security.

He was at Oxford's Programming Research Group from 1982-99, and has since 2000 been at the University of New South Wales.