Axiomatic validation of memory barriers and atomic instructions [LWN.net] edit / delete

More progress on model checking for memory models on modern processors. The tool described here covers ARM, Power and x86 memory models, and does efficient analysis of (smallish) chunks of code.

to arm atomic concurrency herd intel memory memory-model model-checking power static-analysis x86 ... on 28 August 2014

IPC Protocols - MozillaWiki edit / delete

Protocol specifications from the Mozilla project (they plan to model-check using SPIN).

to concurrency ipc model-checking mozilla spin ... on 03 April 2012

McErlang edit / delete

Model-checker for Erlang, using a modified runtime library (much like Neil's CHP-to-CSP trick).

to concurrency erlang model-checking ... on 01 June 2009

Browser bookmarks: tasty+ | tasty= Log in | Export | Atom