Items with a check mark ([Check]) come with a mechanized proof in either Coq or Isabelle/HOL.

See also: [Publications chronologically] [DBLP] [GoogleScholar]

Semantics of weak memory consistency

Program logics for weak consistency

Program logics for sequential consistency

Automated verification of concurrent programs

Interactive theorem proving (Coq)

Verified compilation

Miscellaneous

Valid XHTML 1.0 Strict