Weak consistency semantics:
WMC verification:
SC verification:
Verified compilation:
Other topics:
Items with a check mark ([Check]) come with a mechanized proof in either Coq or Isabelle/HOL.

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

Weak consistency semantics

Weak memory models

Transactional and persistence semantics

Verification under weak memory consistency

Program logics

Automated verification

Verification under Sequential consistency

Program logics

Automated verification

Verified compilation

For sequential programs

For concurrent programs

Other

Interactive theorem proving (Coq)

Miscellaneous

Imprint | Data protection