4 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…
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)…
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…