Formalising Java's Data Race Free Guarantee. - David Aspinall 001; Jaroslav Sevcík (TPHOLs, 2007)

Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers. - Jaroslav Sevcík (Bytecode@ETAPS, 2007)

On Validity of Program Transformations in the Java Memory Model. - Jaroslav Sevcík; David Aspinall 001 (ECOOP, 2008)

Program transformations in weak memory models. - Jaroslav Sevcík (2009)

Safe optimisations for shared-memory concurrent programs. - Jaroslav Sevcík (PLDI, 2011)

Relaxed-memory concurrency and verified compilation. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (POPL, 2011)

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (J. ACM, 2013)

Spectre is here to stay: An analysis of side-channels and speculative execution. - Ross McIlroy; Jaroslav Sevcík; Tobias Tebbi; Ben L. Titzer; Toon Verwaest (CoRR, 2019)