21 citations · 37 across the 5 of their papers we have counts for
5 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.…
Verifying Fault-Tolerance of Quantum Error Correction Codes
Kean Chen, Yuhao Liu, Wang Fang +5
Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC)…
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…