Personal information

Verified email domains

Activities

Employment (1)

Inria: Lyon, FR

Research
Employment
Source: Self-asserted source
Yannick Zakowski

Works (9)

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

Proceedings of the ACM on Programming Languages
2024-08-15 | Journal article
Contributors: Calvin Beck; Irene Yoon; Hanxi Chen; Yannick Zakowski; Steve Zdancewic
Source: check_circle
Crossref

Abstract Interpreters: A Monadic Approach to Modular Verification

Proceedings of the ACM on Programming Languages
2024-08-15 | Journal article
Contributors: Sébastien Michelland; Yannick Zakowski; Laure Gonnord
Source: check_circle
Crossref

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

Proceedings of the ACM on Programming Languages
2023-01-09 | Journal article
Contributors: Nicolas Chappe; Paul He; Ludovic Henrio; Yannick Zakowski; Steve Zdancewic
Source: check_circle
Crossref

Formal reasoning about layered monadic interpreters

Proceedings of the ACM on Programming Languages
2022-08-29 | Journal article
Contributors: Irene Yoon; Yannick Zakowski; Steve Zdancewic
Source: check_circle
Crossref

Modular, compositional, and executable formal semantics for LLVM IR

Proceedings of the ACM on Programming Languages
2021-08-22 | Journal article
Contributors: Yannick Zakowski; Calvin Beck; Irene Yoon; Ilia Zaichuk; Vadim Zaliva; Steve Zdancewic
Source: check_circle
Crossref

Interaction trees: representing recursive and impure programs in Coq

Proceedings of the ACM on Programming Languages
2020-01 | Journal article
Part of ISSN: 2475-1421
Contributors: Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic
Source: Self-asserted source
Yannick Zakowski

An equational theory for weak bisimulation via generalized parameterized coinduction

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
2020-01-20 | Conference paper
Contributors: Yannick Zakowski; Paul He; Chung-Kil Hur; Steve Zdancewic
Source: Self-asserted source
Yannick Zakowski

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

Journal of Automated Reasoning
2019-08 | Journal article
Contributors: Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek
Source: check_circle
Crossref

Verified compilation of linearizable data structures

Proceedings of the 33rd Annual ACM Symposium on Applied Computing
2018-04-09 | Conference paper
Contributors: Yannick Zakowski; David Cachera; Delphine Demange; David Pichardie
Source: Self-asserted source
Yannick Zakowski