A Constructive Theory of Regular Languages in Coq. - Christian Doczkal; Jan-Oliver Kaiser; Gert Smolka (CPP, 2013)

Pilsner: a compositionally verified compiler for a higher-order imperative language. - Georg Neis; Chung-Kil Hur; Jan-Oliver Kaiser; Craig McLaughlin; Derek Dreyer; Viktor Vafeiadis (ICFP, 2015)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2017)

Mtac2: typed tactics for backward reasoning in Coq. - Jan-Oliver Kaiser; Beta Ziliani; Robbert Krebbers; Yann Régis-Gianas; Derek Dreyer (Proc. ACM Program. Lang., 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

RustBelt meets relaxed memory. - Hoang-Hai Dang; Jacques-Henri Jourdan; Jan-Oliver Kaiser; Derek Dreyer (Proc. ACM Program. Lang., 2020)

Modular, Full-System Verification. - Gregory Malecha; Hoang-Hai Dang; Paolo G. Giarrusso; Simon Hudon; Jan-Oliver Kaiser; David Swasey (HotOS, 2025)