I am seeking exceptional math-inclined candidates who are interested (and preferably have experience) in one or more of the following topics:

– weakly consistent memory models (a.k.a. relaxed memory models)
– weak consistency in distributed key-value stores
– verification of concurrent programs and proof techniques for linearizability and contextual refinement
– dynamic analysis of concurrent programs
– the Coq proof assistant