University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Nitpicking C++ Concurrency

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Nitpicking C++ Concurrency

Download to your calendar using vCal

If you have a question about this talk, please contact Tjark Weber .

Previous work formalized the C++ memory model in Isabelle/HOL in an effort to clarify the proposed standard’s semantics. Here we employ the model finder Nitpick to check litmus test programs that exercise the memory model, including a simple locking algorithm. Nitpick is built on Kodkod (Alloy’s backend) but understands Isabelle’s richer logic; hence it can be applied directly to the C++ memory model. We only need to give it a few hints, and thanks to the underlying SAT solver it scales much better than the Cppmem explicit-state model checker. This case study inspired optimizations in Nitpick from which other formalizations can now benefit.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Seminar Room 5, Cripps Court, Magdalene College Chapel, Robinson College, Cambridge Demo Room One, Demo Building

Other talks

Loke CTR Annual Meeting 2026 - Epigenetics of embryogenesis and placentation Talk TBC Title to be confirmed Title to be confirmed Group Presentation 4 The Neurophenomenology of Surrender: Agency, Renewal, and Social Engagement in Speaking in Tongues
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity