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

Imprint | Data protection