On the Feasibility of a Technological Response to the Surveillance Morass. - Joan Feigenbaum; Jérémie Koenig (Security Protocols Workshop, 2014)

On the Feasibility of a Technological Response to the Surveillance Morass (Transcript of Discussion). - Joan Feigenbaum; Jérémie Koenig (Security Protocols Workshop, 2014)

A Compositional Semantics for Verified Separate Compilation and Linking. - Tahina Ramananandro; Zhong Shao 001; Shu-Chun Weng; Jérémie Koenig; Yuchen Fu (CPP, 2015)

Deep Specifications and Certified Abstraction Layers. - Ronghui Gu; Jérémie Koenig; Tahina Ramananandro; Zhong Shao 001; Xiongnan (Newman) Wu; Shu-Chun Weng; Haozhong Zhang; Yu Guo (POPL, 2015)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

Risk based planning of network changes in evolving data centers. - Omid Alipourfard; Jiaqi Gao; Jérémie Koenig; Chris Harshaw; Amin Vahdat; Minlan Yu (SOSP, 2019)

Building certified concurrent OS kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Jieung Kim; Jérémie Koenig; Xiongnan (Newman) Wu; Vilhelm Sjöberg; David Costanzo (Commun. ACM, 2019)

Refinement-Based Game Semantics for Certified Abstraction Layers. - Jérémie Koenig; Zhong Shao 001 (LICS, 2020)

CompCertO: compiling certified open C components. - Jérémie Koenig; Zhong Shao 001 (PLDI, 2021)

Grounding Game Semantics in Categorical Algebra. - Jérémie Koenig (ACT, 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

Layered and object-based game semantics. - Arthur Oliveira Vale; Paul-André Melliès; Zhong Shao 001; Jérémie Koenig; Léo Stefanesco (Proc. ACM Program. Lang., 2022)

Verified compilation of C programs with a nominal memory model. - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Proc. ACM Program. Lang., 2022)

A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. - Ling Zhang; Yuting Wang 001; Jérémie Koenig; Zhong Shao 001 (CoRR, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. - Jieung Kim; Jérémie Koenig; Hao Chen 023; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. - Yu Zhang 086; Jérémie Koenig; Zhong Shao 001; Yuting Wang 001 (Proc. ACM Program. Lang., 2025)