Yannick Zakowski

According to our database, Yannick Zakowski authored at least 21 papers between 2017 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

HELIX: Verified compilation of cyber-physical control systems to LLVM IR.

Vadim Zaliva, Yannick Zakowski, Ilia Zaichuk, Valerii Huhnin, Calvin Beck, Irene Yoon, Steve Zdancewic

CoRR, April, 2026

Layers of Confluence for Actors.

Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

Structural Temporal Logic for Mechanized Program Verification.

Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel

Proc. ACM Program. Lang., 2025

Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq.

Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic

J. Funct. Program., 2025

Front Matter, Table of Contents, Preface, Conference Organization.

Karine Even-Mendoza, Raphaël Monat, Yannick Zakowski

Dagstuhl Artifacts Ser., 2025

Artifact Report: an Abstract, Certified Account of Operational Game Semantics.

Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski

Proceedings of the Programming Languages and Systems, 2025

An abstract, certified account of operational game semantics.

Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski

Proceedings of the Programming Languages and Systems, 2025

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR.

Nicolas Chappe, Ludovic Henrio, Yannick Zakowski

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

2024

Abstract Interpreters: A Monadic Approach to Modular Verification.

Sébastien Michelland, Yannick Zakowski, Laure Gonnord

Proc. ACM Program. Lang., 2024

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction.

Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic

Proc. ACM Program. Lang., 2024

A Two-Phase Infinite/Finite Low-Level Memory Model.

Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic

CoRR, 2024

2023

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.

Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic

Proc. ACM Program. Lang., January, 2023

2022

Formal reasoning about layered monadic interpreters.

Irene Yoon, Yannick Zakowski, Steve Zdancewic

Proc. ACM Program. Lang., 2022

2021

Modular, compositional, and executable formal semantics for LLVM IR.

Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic

Proc. ACM Program. Lang., 2021

2020

Interaction trees: representing recursive and impure programs in Coq.

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic

Proc. ACM Program. Lang., 2020

An equational theory for weak bisimulation via generalized parameterized coinduction.

Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology.

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

J. Autom. Reason., 2019

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic

CoRR, 2019

2018

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie

Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

2017

Verification of a Concurrent Garbage Collector. (Vérification d'un glaneur de cellules concurrent).

Yannick Zakowski

PhD thesis, 2017

Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017