Modular, compositional, and executable formal semantics for LLVM IR

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

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-30. ⟨10.1145/3473572⟩

International audience; This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be7b231401a844d53f3deaa6fe4dd409
https://doi.org/10.1145/3473572

Interaction trees: representing recursive and impure programs in Coq

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

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-32. ⟨10.1145/3371119⟩
Xia, L, Zakowski, Y, He, P, Hur, C-K, Malecha, G, Pierce, B C & Zdancewic, S 2019, ' Interaction Trees: Representing Recursive and Impure Programs in Coq ', Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, 51 . https://doi.org/10.1145/3371119

"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::980af888520ab46c18a347e22f031f1d
https://doi.org/10.1145/3371119

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

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

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩
Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9489-x⟩

International audience; Concurrent garbage collection algorithms are a challenge for program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the Rely-Guarantee proof technique. We design a com

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::385df8e2609d466368827576019acb7a
https://hal.science/hal-01897251/file/jar18.pdf

Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

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

Publikováno v: ITP 2017-8th International Conference on Interactive Theorem Proving
ITP 2017-8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving ISBN: 9783319661063
ITP
J. Autom. Reasoning

International audience; Concurrent garbage collection algorithms are an emblematic challenge in the area of concurrent program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the popular Rely-

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5548be8beb952f52abdbda285872812d
https://hal.inria.fr/hal-01613389