21 citations · 37 across the 5 of their papers we have counts for
4 papers · 1 filter
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…