Yannick Zakowski

According to our database, Yannick Zakowski authored at least 14 papers between 2017 and 2024.

Collaborative distances:

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

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

Structural temporal logic for mechanized program verification.

Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel

CoRR, 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