LMS/BCS-FACS Seminar 2025
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. These events are free to anyone who wishes to attend and have attracted high-quality speakers
We will endeavour to upload the talks to the LMS YouTube channel - click 'subscribe' to be alerted when new videos are added.
Programme (all times in GMT)
The event will start promptly at 19:00.
Speaker: Annabelle McIver (Macquarie University)
Bio: 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”.
Title: Probabilistic Datatypes: automating verification for abstract probabilistic reasoning
Abstract: 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.
Chair/facilitator: Andrei Popescu (University of Sheffield)
Accessibility
This event is online only and will be streamed via Zoom.
Closed captions will be enabled on Zoom, and we will endeavour to upload this to our LMS YouTube channel as soon as possible after the event.
If you have any accessibility questions not covered by the above, please contact lmscomputerscience@lms.ac.uk.
Registration
-
To attend remotely via Zoom, please complete the registration form here. You will receive the link to the meeting upon registration, as well as an automated reminder email sent 24 hours before the event is scheduled to start.
-
For all queries regarding the seminar, please contact lmscomputerscience@lms.ac.uk.