131 citations · 177 across the 6 of their papers we have counts for
6 papers
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
Vadim Zaliva, Yannick Zakowski, Ilia Zaichuk +4
This paper presents the design of HELIX, an end-to-end verified code generation system with a focus on the intersection of high-performance and high-assurance numerical computing.…
Structural Temporal Logic for Mechanized Program Verification
Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic +1
Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of…
A Two-Phase Infinite/Finite Low-Level Memory Model
Calvin Beck, Irene Yoon, Hanxi Chen +2
This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer--integer casts, with desired refinements that are needed to justify the…
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Nicolas Chappe, Paul He, Ludovic Henrio +2
This paper introduces Choice Trees (ctrees), a monad for modeling nondeterministic, recursive, and impure programs in Coq. Inspired by Xia et al.'s itrees, this novel data structur…
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur +1
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning princi…
Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He +4
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant…