In association with the British Computer Society Formal Aspects of Computing Science (BCS-FACS), the LMS hosts an annual online seminar on aspects of the computer science–mathematics interface.
Agenda
7:00pm - Event start
8:00pm - Event close
Synopsis
Probabilistic Datatypes: automating verification for abstract probabilistic reasoning
Datatypes - in which data is encapsulated together with methods that access it - play an important role in the organisation of large software projects. Correctness of datatypes has traditionally been carried out using simulation relations to simplify the verification by separating concerns: the datatype can be verified independently from the programs that use it, whilst those programs themselves can be verified using the specifications of the datatype's methods. Use of these principles enables complex programs to be brought within reach of automated proof.
When probabilistic choice is included, however, it turns out that obtaining similar simplifications of the verification problem will require distinguishing between "hidden" and "observable" probabilistic behaviour - if demonic choice is allowed in the surrounding program. And that is not required in the non-probabilistic setting: the crucial issue is the potential interaction of probabilistic- and demonic choice.
In the main part of this talk I will use examples to explain why the interaction is problematic, and I will suggest how extension of existing pGCL-based automated reasoning-tools, will by taking that interaction into account, enable automated probabilistic abstract reasoning about "hard to crack" probabilistic programs.
About the speaker
Annabelle McIver
Annabelle McIver is a professor of Computer Science at Macquarie University in Sydney, and co-director of the Future Communications Research Centre. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book "Abstraction, Refinement and Proof for Probabilistic Systems", and "The Science of Quantitative Information Flow”.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.
This event is brought to you by: FACS (Formal Aspects of Computing Science) group and LMS
