COMING SOON! PQDT Open is getting a new home!

ProQuest Open Access Dissertations & Theses will remain freely available as part of a new and enhanced search experience at www.proquest.com.

Questions? Please refer to this FAQ.

Dissertation/Thesis Abstract

HELIX: From Math to Verified Code
by Zaliva, Vadim, Ph.D., Carnegie Mellon University, 2020, 201; 28262508
Abstract (Summary)

This thesis presents HELIX, a code generation and formal verification system with a focus on the intersection of high-performance and high-assurance numerical computing. This allowed us to build a system that could be fine-tuned to generate efficient code for a broad set of computer architectures while providing formal guarantees of such generated code's correctness.

The method we used for high-performance code synthesis is the algebraic transformation of vector and matrix computations into a data flow optimized for parallel or vectorized processing on target hardware. The abstraction used to formalize and verify this technique is an operator language used with semantics-preserving term-rewriting. We use sparse vector abstraction to represent partial computations, enabling us to use algebraic reasoning to prove parallel decomposition properties.

HELIX provides a formal verification foundation for rewriting-based algebraic code synthesis optimizations, driven by an external oracle. Presently HELIX uses SPIRAL as an oracle deriving the rule application order. The SPIRAL system was developed over the years and successfully applied to generate code for various numeric algorithms. Building on its sound algebraic foundation, we generalize and extend it in the direction of non-linear operators, towards a new theory of partial computations, applying formal language theory and formal verification techniques.

HELIX is developed and proven in Coq proof assistant and demonstrated on a real-life example of verified high-performance code generation of the dynamic window safety monitor for a cyber-physical robot system.

Indexing (document details)
Advisor: Franchetti, Franz
Commitee: Pasareanu, Corina, Jia, Limin, Zdancewic, Steve
School: Carnegie Mellon University
Department: Electrical and Computer Engineering
School Location: United States -- Pennsylvania
Source: DAI-B 82/7(E), Dissertation Abstracts International
Source Type: DISSERTATION
Subjects: Computer science, Computer Engineering
Keywords: Coq, Cyber-physical systems, Formal semantics, Formal verification, High-assurance, High-performance
Publication Number: 28262508
ISBN: 9798569901869
Copyright © 2021 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy
ProQuest