Skip to main content

Deductive Verification under the C11 Memory Model

Seminar by Brijesh Dongol (University of Surrey)

  • Date 24 Feb 2021
  • Time 3.00pm-4.00pm
  • Category Seminar

Deductive Verification under the C11 Memory Model

Abstract: Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference-freedom rule for concurrency. This talk describes a Hoare logic for a fragment of the C11 memory model that includes both relaxed and release-acquire accesses. Our logic features novel assertions on thread-specific views and a set of Hoare logic axioms that describe how these assertions are affected by atomic program steps. Our framework is such that the standard Owicki-Gries proof rules for compound statements, including non-interference remain unchanged. We demonstrate the utility of our framework by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in Isabelle/HOL. If time permits, I will discuss recent efforts to verify refinement under C11 and the verification of C11 library abstractions.

This is joint work with Sadegh Dalvandi, Simon Doherty, and Heike Wehrheim.

Bio: Brijesh Dongol is Senior Lecturer at the University of Surrey. He has a BSc in Computer Science and Mathematics and a BSc (Hons) in Logic and Computation, both from Victoria University of Wellington, New Zealand. In 2009, he received a PhD on formal derivations of concurrent algorithms at the University of Queensland, Australia. After this, he held postdoctorate positions at the University of Queensland and then at the University of Sheffield. He was a lecturer at Brunel University London (2014-18). 

brijesh-pic.jpg

Related topics

Explore Royal Holloway

Get help paying for your studies at Royal Holloway through a range of scholarships and bursaries.

There are lots of exciting ways to get involved at Royal Holloway. Discover new interests and enjoy existing ones.

Heading to university is exciting. Finding the right place to live will get you off to a good start.

Whether you need support with your health or practical advice on budgeting or finding part-time work, we can help.

Discover more about our academic departments and schools.

Find out why Royal Holloway is in the top 25% of UK universities for research rated ‘world-leading’ or ‘internationally excellent’.

Royal Holloway is a research intensive university and our academics collaborate across disciplines to achieve excellence.

Discover world-class research at Royal Holloway.

Discover more about who we are today, and our vision for the future.

Royal Holloway began as two pioneering colleges for the education of women in the 19th century, and their spirit lives on today.

We’ve played a role in thousands of careers, some of them particularly remarkable.

Find about our decision-making processes and the people who lead and manage Royal Holloway today.