pith. machine review for the scientific record. sign in

arxiv: 2604.18593 · v1 · submitted 2026-03-27 · 💻 cs.PL

Recognition: 2 theorem links

· Lean Theorem

HELIX: Verified compilation of cyber-physical control systems to LLVM IR

Vadim Zaliva , Yannick Zakowski , Ilia Zaichuk , Valerii Huhnin , Calvin Beck , Irene Yoon , Steve Zdancewic
Authors on Pith no claims yet

Pith reviewed 2026-05-14 22:08 UTC · model grok-4.3

classification 💻 cs.PL
keywords verified compilationcyber-physical systemsLLVM IRterm rewritingalgebraic transformationsCoqnumerical computingsemantic preservation
0
0 comments X

The pith

HELIX generates verified LLVM IR code from high-level mathematical models of cyber-physical systems by applying algebraic transformations with formal semantic preservation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents HELIX as an end-to-end verified code generation system that starts from a high-level mathematical formulation of a cyber-physical control problem. It applies a series of algebraic transformations on vector and matrix computations, targeting intermediate languages, to produce an efficient imperative implementation. All transformations are formally verified to preserve semantics down to LLVM IR using the Coq proof assistant. The approach relies on an operator language with term rewriting rules and sparse vector abstractions to support optimizations like parallel or vectorized processing. A running example of a real robot system illustrates the full pipeline from math to executable code.

Core claim

HELIX shows that vector and matrix computations in cyber-physical systems can be formalized in an operator language whose semantics-preserving term rewriting rules, combined with sparse vector abstraction for partial computations, enable verified algebraic transformations that turn high-level mathematical specifications into optimized LLVM IR while guaranteeing semantic equivalence throughout the process.

What carries the argument

Operator language with semantics-preserving term rewriting rules and sparse vector abstraction that formalizes algebraic transformations of vector and matrix computations into optimized dataflow for parallel processing.

If this is right

  • High-level mathematical models of cyber-physical systems can be transformed into architecture-specific efficient code while retaining formal correctness proofs.
  • Sparse vector representations allow algebraic proofs of parallel decomposition properties that improve performance on vectorized or parallel hardware.
  • The multi-layered verification approach in Coq, including term rewriting and translation validation, scales to full systems from math down to LLVM IR.
  • Application-specific numerical analysis can be integrated into the verified pipeline without breaking semantic guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same operator-language approach could be applied to other numerical domains such as signal processing or optimization problems that involve similar matrix transformations.
  • Extending the rewriting rules to include additional hardware-specific optimizations might reduce the need for manual tuning while keeping verification intact.
  • Adapting the system to generate code for new target architectures would require only extending the final translation step, provided the intermediate semantics remain unchanged.

Load-bearing premise

The operator language semantics and term rewriting rules correctly capture and preserve the meaning of the original vector and matrix computations in the cyber-physical system.

What would settle it

Execute the LLVM IR generated by HELIX from the robot system example on the same inputs used in the high-level mathematical formulation and observe whether the outputs match exactly.

Figures

Figures reproduced from arXiv: 2604.18593 by Calvin Beck, Ilia Zaichuk, Irene Yoon, Steve Zdancewic, Vadim Zaliva, Valerii Huhnin, Yannick Zakowski.

Figure 1
Figure 1. Figure 1: HELIX transformation stages Presently, HELIX works together with SPIRAL, which it uses as an Oracle. SPIRAL, using its extensive library of (unverified) algorithms and heuristics, decides how the original expression will be compiled into optimal code. HELIX mirrors corresponding SPIRAL transformations, adding formal verification assurances (translation validation approach [64]). The HELIX input language, c… view at source ↗
Figure 2
Figure 2. Figure 2: HELIX chain of verification 4Both FHCOL and VIR use the Compcert-style memory model with integer-indexed memory blocks that contain integer-indexed memory cells. The only difference is that FHCOL memory cells are floats, while VIR’s are bytes [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: HELIX application to high-assurance vehicle control [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: HPointwise operator Let us look more closely at the definition of the HPointwise operator in Coq: Definition HPointwise {n: N} (f: I𝑛 → R → R) (x: vector R n) : vector R n := Vbuild (𝜆 j jd ⇒ f (mkFinNat jd) (Vnth x jd)). Listing 1. HPointwise operator definition [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Dynamic Window Monitor dataflow graph in [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: HELIX translation validation of SPIRAL HCOL rewriting This approach, shown in [PITH_FULL_IMAGE:figures/full_fig_p020_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Dense vector as sum of four sparse vectors [PITH_FULL_IMAGE:figures/full_fig_p021_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Dense vector as sum of two sparse vectors [PITH_FULL_IMAGE:figures/full_fig_p021_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Map-Reduce of a sparse embedding expression can be gradually transferred to a purely functional form by applying a series of rewriting rules. In iterative factorization of operations on vectors, each iteration represents a partial computation which outputs a sparse vector. In SPIRAL, the sparsity is represented by default values (typically 0) assigned to sparse cells. No tracking is performed which histori… view at source ↗
Figure 10
Figure 10. Figure 10: Sparse vectors as dictionaries Generally speaking, there is a 1-to-1 correspondence between Σ-HCOL and MSHCOL operators with the main difference in the input and output container data types. MSHCOL uses memory blocks, where Σ-HCOL uses sparse vectors. An example application of the MApply2Union operator in MSHCOL is shown in [PITH_FULL_IMAGE:figures/full_fig_p031_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: MApply2Union in MSHCOL With this change of data representation, we move away from the algebraic nature of Σ-HCOL towards a lower-level representation. In this representation, an actual value must be associated with a key in a dictionary before it can be accessed. Trying to access an uninitialized key is an error. It means that MSHCOL operators could return errors and thus have the type: mem block → option… view at source ↗
Figure 12
Figure 12. Figure 12: Syntax of AExpr expressions Syntax for DHCOL operators is shown in [PITH_FULL_IMAGE:figures/full_fig_p037_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Syntax of DHCOL operators Example of a DHCOL operator, DSHIMap. Detailed description of all DHCOL operators can be found in Appendix D.2. DSHIMap (n: N) (x y: PExpr) (f: AExpr). It iterates the index from 0 to 𝑛 − 1. For each iteration, the values from x at the index offset are added to the evaluation context, and the expression f is evaluated. It could be viewed as calling function 𝑓 with the two argumen… view at source ↗
Figure 14
Figure 14. Figure 14: Variable resolver example 5.5.2 Proof of semantics preservation While the regular MSHCOL operators translate to a RHCOL program fragment, the higher￾order operators translate into a sequence of instructions, with placeholders filled with RHCOL translations of their respective parameters. For example, MSHCOL’s (MSHIReduction i o n z f op family) operator is compiled to the following RHCOL program: DSHSeq (… view at source ↗
Figure 15
Figure 15. Figure 15: shows the origin of these values in a case where no errors occur. Legend: 𝜎 is an evaluation context, and m and m ′ are memory states before and after execution of the evalDSHOperator. The ma corresponds to a memory block in m ′ referenced by y p. The md is the result of applying the MSHCOL operator to mx [PITH_FULL_IMAGE:figures/full_fig_p044_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Vellvm: Levels of interpretation details by [88]. The fork in the stack happens where non-determinism comes into play: the semantics itself (the left path) captures sets of valid computations, while a deterministic, executable, alternative (the right path) is provided for testing purposes, and proved against the semantics to be a valid execution. Crucially, each level of the layer induces its own notion o… view at source ↗
Figure 17
Figure 17. Figure 17: Relational reasoning principles While this notation provides the right intuition, we keep things more shallow in our formal development as our language of assertions itself is shallow, and as we need to work at various levels of denotation whose types differ slightly [PITH_FULL_IMAGE:figures/full_fig_p063_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: Structural VIR equations (excerpt) outputs(𝑏𝑘 𝑠2) ∩ inputs(𝑏𝑘 𝑠1) = ∅ 𝑏𝑠 ∉ inputs(𝑏𝑘 𝑠1) Jbks1 ++ bks2Kbks (𝑏 𝑓 , 𝑏𝑠) ≈ Jbks2Kbks (𝑏 𝑓 , 𝑏𝑠) OcfgSeq1 outputs(𝑏𝑘 𝑠2) ∩ inputs(𝑏𝑘 𝑠1) = ∅ Jbks1 ++ bks2Kbks (𝑏 𝑓 , 𝑏𝑠) ≈ 𝑓 𝑜𝑣 ← Jbks1Kbks (𝑏 𝑓 , 𝑏𝑠) ;; tryret 𝑓 𝑜𝑣 in Jbks2Kbks OcfgSeq2 independent 𝑏𝑘 𝑠1 𝑏𝑘 𝑠2 𝑏𝑠 ∈ inputs(𝑏𝑘 𝑠1) Jbks1 ++ bks2Kbks (𝑏 𝑓 , 𝑏𝑠) ≈ Jbks1Kbks (𝑏 𝑓 , 𝑏𝑠) OcfgBrL independent 𝑏𝑘 𝑠1 𝑏𝑘 𝑠2 … view at source ↗
Figure 19
Figure 19. Figure 19: VIR proof rules for reasoning about open programs Finally, we provide atomic semantic rules for VIR expressions, instructions, and terminators – a minimal excerpt is provided on [PITH_FULL_IMAGE:figures/full_fig_p064_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Specifications for VIR (excerpt) All put together, this proof theory achieves several goals. First, it allows us to keep the representation functions and interpreters opaque, hiding their internal representation as itrees, recovering reasonably performant and convenient setoid-based rewrites when reasoning about VIR’s syntax. Second, it lifts the reasoning to the level of syntactic VIR program, i.e., yiel… view at source ↗
Figure 21
Figure 21. Figure 21: Global pointer memory invariant For each variable stored in 𝜎, the invariant expresses how the static context Γ associates a VIR identifier storing in memory the same data—the details of this mapping depends on the type of data concerned [PITH_FULL_IMAGE:figures/full_fig_p069_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Comparing two imprecise values can be unsafe if their error bounds intersect. [PITH_FULL_IMAGE:figures/full_fig_p076_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: It is safe to compare two imprecise values of sufficiently different magnitudes, as the error [PITH_FULL_IMAGE:figures/full_fig_p076_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: DynWin safety margin on the robot’s plane [PITH_FULL_IMAGE:figures/full_fig_p077_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: A screenshot of the compiler test suite execution [PITH_FULL_IMAGE:figures/full_fig_p080_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: HPointwise operator HAtomic ( 𝑓 : R → R): R 1 → R1 . This operator “lifts” a scalar valued function 𝑓 to an HCOL operator on single element vectors. HScalarProd (𝑛: N): R 𝑛+𝑛 → R1 . Calculates the dot product of two vectors. The input vectors must be concatenated and passed as a single vector of size 𝑛 + 𝑛. The result is [PITH_FULL_IMAGE:figures/full_fig_p087_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: HBinOp operator HReduction (𝑛: N) ( 𝑓 : R → R → R) (𝑧: R): R 𝑛 → R1 . This operator performs a right fold of a vector. The two parameters are a binary function 𝑓 and the initial value 𝑧. The result is returned as a vector size 1. HEvalPolynomial (𝑛: N) ( ®𝑎 : R 𝑛 ): R 1 → R1 . This operator computes a univariate poly￾nomial of an 𝑛-th degree. It is parameterized by a vector 𝑎® of constant coefficients. Th… view at source ↗
Figure 28
Figure 28. Figure 28: Embed dataflow Pick (𝑠: R) (𝑛 𝑏 : N) (𝑏𝑐 : 𝑏 < 𝑛): SHOperator 𝑓 𝑚 𝑛 1 𝑠. Selects an element from the input vector at the given index 𝑏 and returns it as a single element vector [PITH_FULL_IMAGE:figures/full_fig_p091_28.png] view at source ↗
Figure 29
Figure 29. Figure 29: Pick dataflow [PITH_FULL_IMAGE:figures/full_fig_p091_29.png] view at source ↗
Figure 30
Figure 30. Figure 30: Scatter dataflow Gather (𝑠: R) (𝑛 𝑚 : N) ( 𝑓 : index map 𝑚 𝑛): SHOperator 𝑓 𝑚 𝑛 𝑚 𝑠. Picking can be generalized where more than one element can be picked at once. The element selection is controlled by a user-provided index mapping function 𝑓 [PITH_FULL_IMAGE:figures/full_fig_p092_30.png] view at source ↗
Figure 31
Figure 31. Figure 31: Gather dataflow liftM HOperator (𝑖 𝑜 : N) (𝑠: R) (𝑜 𝑝 : avecotr 𝑖 → avector 𝑜): SHOperator 𝑓 𝑚 𝑖 𝑜 𝑠. This operator allows “lifting” HCOL operators, so they can be used in Σ-HCOL expressions. Since HCOL operates on dense vectors, the input vector is first “densified” by dropping structural flags and replacing sparse values with the 𝑠. During this operation, structural values become indistinguishable from … view at source ↗
Figure 32
Figure 32. Figure 32: Apply2Union dataflow The additional constraint is that the default value for sparse cells (𝑠) is a fixpoint of the provided binary function 𝑑𝑜𝑡, defined as 𝑑𝑜𝑡(𝑠, 𝑠) = 𝑠. This is to assure that the value of sparse cells is preserved when combining them. SafeCast (𝑠: R) (𝑖 𝑜 : N) ( 𝑓 : SHOperator Monoid R ′ flags𝑖 𝑜 𝑠): SHOperator Monoid Rflags 𝑖 𝑜 𝑠. This is a higher-order operator wrapping another Σ-HCOL… view at source ↗
read the original abstract

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. The code generation can be fine-tuned to generate efficient code for a broad set of computer architectures while providing formal guarantees of the correctness of such generated code. Using a real-life example of a cyber-physical robot system, this paper demonstrates how, by using HELIX, one can start from a high-level mathematical formulation of the problem, apply a series of algebraic transformations that target intermediate languages, and generate an efficient imperative implementation. This is done while formally verifying semantic preservation from the original formulation down to LLVM IR. The method we used for high-performance code compilation is the algebraic transformation of vector and matrix computations into a dataflow optimised for parallel or vectorised processing on target hardware. The abstraction used to formalise and verify this technique is an operator language and accompanying 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's verification infrastructure comprises multiple intermediate languages and verification approaches, all implemented in the Coq proof assistant. In particular, it uses verified term rewriting, translation validation, metaprogramming, verified compilation, layered monadic interpreters; it also supports application-specific uses of (verified) numerical analysis as we demonstrate via the running example.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces HELIX, an end-to-end verified compilation framework implemented in Coq for generating efficient LLVM IR code from high-level mathematical descriptions of cyber-physical control systems. It employs an operator language with term-rewriting rules based on sparse vector abstractions to perform algebraic optimizations for parallel and vectorized execution, using a robot control system as a running example to demonstrate semantic preservation from the original formulation through intermediate languages to LLVM IR via verified transformations, metaprogramming, and translation validation.

Significance. If the formal guarantees hold as claimed, this work would represent a significant advance in verified high-performance computing for safety-critical cyber-physical systems. By combining algebraic reasoning over sparse computations with a multi-layered Coq verification infrastructure, it offers a practical path from mathematical models to optimized machine code with machine-checked correctness proofs, addressing a key gap in high-assurance numerical software development.

major comments (2)
  1. The central claim that the operator language semantics and term-rewriting rules correctly capture and preserve meaning for sparse partial evaluations (including interactions with matrix multiplications) is load-bearing for the entire verification chain, yet the manuscript provides no proof sketches, confluence/termination arguments, or explicit handling of floating-point associativity assumptions for the patterns arising in the robot control example.
  2. § on verification infrastructure: while the paper lists verified term rewriting, translation validation, metaprogramming, and layered monadic interpreters, no specific theorem statements or coverage arguments are given showing that all algebraic transformations and sparse decompositions are accounted for in the Coq development.
minor comments (1)
  1. The abstract would be strengthened by briefly indicating the scale of the robot control example (e.g., matrix dimensions or number of transformations) to help readers gauge the practicality of the approach.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive comments, which help clarify the presentation of our formal results. We address each major comment below, indicating planned revisions to strengthen the manuscript while preserving its core contributions.

read point-by-point responses

  1. Referee: The central claim that the operator language semantics and term-rewriting rules correctly capture and preserve meaning for sparse partial evaluations (including interactions with matrix multiplications) is load-bearing for the entire verification chain, yet the manuscript provides no proof sketches, confluence/termination arguments, or explicit handling of floating-point associativity assumptions for the patterns arising in the robot control example.

    Authors: We acknowledge that the manuscript does not include explicit proof sketches, confluence/termination arguments, or a dedicated discussion of floating-point associativity assumptions. The full semantic preservation proofs for the operator language, term-rewriting rules, and sparse vector abstractions (including matrix interactions) are formalized in the accompanying Coq development. In the revised manuscript we will add a new subsection with proof sketches for the key theorems, a brief argument for termination and confluence based on the well-founded ordering induced by the sparse representation, and an explicit statement of the floating-point assumptions used in the robot control example (commutativity of addition and multiplication under the verified error bounds). revision: yes

  2. Referee: § on verification infrastructure: while the paper lists verified term rewriting, translation validation, metaprogramming, and layered monadic interpreters, no specific theorem statements or coverage arguments are given showing that all algebraic transformations and sparse decompositions are accounted for in the Coq development.

    Authors: We agree that the manuscript would benefit from more explicit theorem statements and coverage arguments. The Coq development contains machine-checked theorems establishing semantic preservation for each layer (term rewriting, translation validation, and monadic interpretation) and for every algebraic transformation and sparse decomposition appearing in the running example. In the revision we will insert a dedicated paragraph listing the principal theorems (e.g., Theorem 4.2: Preservation of sparse partial evaluation; Theorem 5.1: End-to-end LLVM IR correctness) together with a short coverage argument explaining how the layered infrastructure accounts for all transformations used in the robot controller. revision: yes

Circularity Check

0 steps flagged

No circularity: verification rests on Coq definitions and external LLVM semantics

full rationale

The derivation chain is self-contained because the operator language, term-rewriting rules, and semantic-preservation proofs are implemented and machine-checked inside Coq; the final translation to LLVM IR is validated against an external, independently defined LLVM semantics rather than being derived from the paper's own outputs or prior self-citations. No step reduces a claimed prediction or uniqueness result to a fitted parameter or to an unverified self-citation; the algebraic transformations are justified by explicit Coq proofs of preservation, not by renaming or smuggling ansatzes.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that the custom operator language and term rewriting accurately model the numerical computations; no free parameters or invented entities are described in the abstract.

axioms (1)
  • domain assumption The operator language semantics accurately capture the computations in cyber-physical systems and the term rewriting preserves those semantics.
    Invoked to justify semantic preservation from math formulation to LLVM IR.

pith-pipeline@v0.9.0 · 5571 in / 1205 out tokens · 55463 ms · 2026-05-14T22:08:34.855804+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

98 extracted references · 98 canonical work pages · 1 internal anchor

  1. [1]

    Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. InThe Third International Workshop on Coq for Programming Languages (CoqPL)

    work page 2017

  2. [2]

    Abhishek Anand and Ross A. Knepper. 2015. ROSCoq: Robots Powered by Constructive Reals. InInteractive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9236), Christian Urban and Xingyuan Zhang (Eds.). Springer, 34–50. doi:10.1007/978-3-319-22102-1 3

    work page doi:10.1007/978-3-319-22102-1 2015

  3. [3]

    Andrew W. Appel. 2011. Verified Software Toolchain. InProgramming Languages and Systems, Gilles Barthe (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–17. doi:10.1007/978-3-642-19718-5 1

    work page doi:10.1007/978-3-642-19718-5 2011

  4. [4]

    Andrew W Appel, Lennart Beringer, Adam Chlipala, Benjamin C Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position paper: the science of deep specification.Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences375, 2104 (2017), 20160331

    work page 2017

  5. [5]

    Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, and Steve Zdancewic. 2024. A Two-Phase Infinite/Finite Low-Level Memory Model.Proc. ACM Program. Lang.ICFP (aug 2024). doi:10.1145/3674652

    work page doi:10.1145/3674652 2024

  6. [6]

    Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. SIGPLAN Not.39, 1 (Jan. 2004), 14–25. doi:10.1145/982962.964003

    work page doi:10.1145/982962.964003 2004

  7. [7]

    Ye, and Andrew W

    Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. InProceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.)(SEC’15). USENIX Association, USA, 207–221. HELIX: Verified compilation of cyber-physical control systems to LLVM IR 117

    work page 2015

  8. [8]

    Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. 2014. Verified Compilation for Shared-Memory C. InESOP (LNCS, Vol. 8410). 107–127. doi:10.1007/978-3-642-54833-8 7

    work page doi:10.1007/978-3-642-54833-8 2014

  9. [9]

    Michael Blair, Sally Obenski, and Paula Bridickas. 1992. Patriot Missile Defense: Software Problem Led to System Failure at Dhahran, Saudi Arabia

    work page 1992

  10. [10]

    Fr´ed´eric Blanqui and Adam Koprowski. 2011. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates.Mathematical Structures in Computer Science21, 4 (2011), 827–859

    work page 2011

  11. [11]

    Myreen, and Andr´e Platzer

    Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and Andr´e Platzer. 2018. VeriPhy: verified controller executables from verified cyber-physical system models. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossma...

    work page doi:10.1145/3192366.3192406 2018

  12. [12]

    Sylvie Boldo, Jean-Christophe Filliˆatre, and Guillaume Melquiond. 2009. Combining Coq and Gappa for certifying floating-point programs. InInternational Conference on Intelligent Computer Mathematics. Springer, 59–74

    work page 2009

  13. [13]

    Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. InComputer Arithmetic (ARITH), 2011 20th IEEE Symposium on. IEEE, 243–252

    work page 2011

  14. [14]

    Peter Borovansk` y, Claude Kirchner, H´elene Kirchner, Pierre-Etienne Moreau, and Christophe Ringeissen

    work page

  15. [15]

    An overview of ELAN.Electronic Notes in Theoretical Computer Science15 (1998), 55–70

    work page 1998

  16. [16]

    Timothy Bourke, L´elio Brun, and Marc Pouzet. 2020. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset. InProceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages(New Orleans, LA, USA), Vol. 4. Association for Computing Machinery. doi:10.1145/3371112

    work page doi:10.1145/3371112 2020

  17. [17]

    Patrick J. Brinich. 2020.Formal Verification of Spiral Generated Code. Master’s thesis. Drexel University

    work page 2020

  18. [18]

    Venanzio Capretta. 2005. General recursion via coinductive types.Log. Methods Comput. Sci.1, 2 (2005). doi:10.2168/LMCS-1(2:1)2005

    work page doi:10.2168/lmcs-1(2:1)2005 2005

  19. [19]

    2012.A gentle introduction to type classes and relations in Coq

    Pierre Cast ´eran and Matthieu Sozeau. 2012.A gentle introduction to type classes and relations in Coq. Technical Report. Technical Report hal-00702455, version 1

    work page 2012

  20. [20]

    Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. 2023. Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.Proc. ACM Program. Lang.7, POPL (2023), 1770–1800. doi:10.1145/3571254

    work page doi:10.1145/3571254 2023

  21. [21]

    Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. 2023. Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.Proceedings of the ACM on Programming Languages7, POPL (2023)

    work page 2023

  22. [22]

    Robert N Charette. 2009. This car runs on code.IEEE spectrum46, 3 (2009), 3

    work page 2009

  23. [23]

    2017.Formal reasoning about programs

    Adam Chlipala. 2017.Formal reasoning about programs. http://adam.chlipala.net/frap

    work page 2017

  24. [24]

    Minki Cho, Youngju Song, Dongjae Lee, Lennard G¨aher, and Derek Dreyer. 2023. Stuttering for Free.Proc. ACM Program. Lang.7, OOPSLA2 (2023), 1677–1704. doi:10.1145/3622857

    work page doi:10.1145/3622857 2023

  25. [25]

    2012.Comparing Floating Point Numbers

    Bruce Dawson. 2012.Comparing Floating Point Numbers. https://randomascii.wordpress.com/2012/02/25/ comparing-floating-point-numbers-2012-edition/

    work page 2012

  26. [26]

    Florent De Dinechin, Christoph Quirin Lauter, and Guillaume Melquiond. 2008. Certifying floating-point implementations using Gappa.arXiv preprint arXiv:0801.0523(2008)

    work page internal anchor Pith review Pith/arXiv arXiv 2008

  27. [27]

    Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. 2017. Combining Model Checking and Runtime Verification for Safe Robotics. InRuntime Verification - 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10548), Shuvendu K. Lahiri and Giles Reger (Eds.). Springer, 172–189. ...

    work page doi:10.1007/978-3-319-67531-2 2017

  28. [28]

    2004.The Coq proof assistant reference manual

    The Coq development team. 2004.The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr Version 8.0

    work page 2004

  29. [29]

    Christof Ebert and Capers Jones. 2009. Embedded Software: Facts, Figures, and Future.Computer42, 4 (April 2009), 42–52. doi:10.1109/MC.2009.118

    work page doi:10.1109/mc.2009.118 2009

  30. [30]

    Simon Foster, Chung-Kil Hur, and Jim Woodcock. 2021. Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. arXiv:2105.05133 [cs.LO]

    work page arXiv 2021

  31. [31]

    Dieter Fox, Wolfram Burgard, and Sebastian Thrun. 1997. The dynamic window approach to collision avoidance.IEEE Robotics & Automation Magazine4, 1 (1997), 23–33. 118 Vadim Zaliva, Yannick Zakowski, Ilia Zaichuk, Valerii Huhnin, Calvin Beck, Irene Yoon, and Steve Zdancewic

    work page 1997

  32. [32]

    Franz Franchetti, Fr´ed´eric de Mesmay, Daniel McFarlin, and Markus P¨ uschel. 2009. Operator Language: A Program Generation Framework for Fast Kernels. InIFIP Working Conference on Domain Specific Languages (DSL WC) (Lecture Notes in Computer Science, Vol. 5658). Springer, 385–410

    work page 2009

  33. [33]

    Franchetti, T

    F. Franchetti, T. M. Low, S. Mitsch, J. P. Mendoza, L. Gui, A. Phaosawasdi, D. Padua, S. Kar, J. M. F. Moura, M. Franusich, J. Johnson, A. Platzer, and M. M. Veloso. 2017. High-Assurance SPIRAL: End-to-End Guarantees for Robot and Car Control.IEEE Control Systems37, 2 (April 2017), 82–103. doi:10.1109/MCS.2016.2643244

    work page doi:10.1109/mcs.2016.2643244 2017

  34. [34]

    From High Level Specification to High Performance Code

    Franz Franchetti, Tze-Meng Low, Thom Popovici, Richard Veras, Daniele G. Spampinato, Jeremy Johnson, Markus P¨ uschel, James C. Hoe, and Jos´e M. F. Moura. 2018. SPIRAL: Extreme Performance Portability. Proceedings of the IEEE, special issue on “From High Level Specification to High Performance Code”106, 11 (2018)

    work page 2018

  35. [35]

    Franz Franchetti and Markus P¨ uschel. 2009. Generating High-Performance Pruned FFT Implementations. In International Conference on Acoustics, Speech, and Signal Processing (ICASSP). 549–552

    work page 2009

  36. [36]

    Franz Franchetti, Markus P¨ uschel, Jos´e M. F. Moura, and Christoph W. Ueberhuber. 2002. Short Vector SIMD Code Generation for DSP Algorithms. InHigh Performance Extreme Computing (HPEC)

    work page 2002

  37. [37]

    Franz Franchetti, Yevgen Voronenko, and Markus P¨ uschel. 2005. Formal Loop Merging for Signal Transforms. InProceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA)(PLDI ’05). ACM, New York, NY, USA, 315–326. doi:10.1145/1065010.1065048

    work page doi:10.1145/1065010.1065048 2005

  38. [38]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus V¨olp, and Andr´e Platzer. 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. InInternational Conference on Automated Deduction. Springer, 527–538

    work page 2015

  39. [39]

    Ronghui Gu, J´er´emie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). ACM, New York, NY, USA, 595–608. doi:10.11...

    work page doi:10.1145/2676726.2676975 2015

  40. [40]

    Bastian Hagedorn, Johannes Lenfers, Thomas Kundefinedhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer. 2020. Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High- Performance Optimizations as Rewrite Strategies.Proc. ACM Program. Lang.4, ICFP, Article 92 (Aug. 2020), 29 pages. doi:10.1145/3408974

    work page doi:10.1145/3408974 2020

  41. [41]

    Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng. 2019. Towards certified separate compilation for concurrent programs. InPLDI. 111–125. doi:10.1145/3314221.3314595

    work page doi:10.1145/3314221.3314595 2019

  42. [42]

    2005.PID control

    Michael A Johnson and Mohammad H Moradi. 2005.PID control. Springer

    work page 2005

  43. [43]

    Rudolph Emil Kalman. 1960. A new approach to linear filtering and prediction problems. (1960)

    work page 1960

  44. [44]

    Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis

    work page

  45. [45]

    InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation(Portland, OR, USA)(PLDI ’15)

    A Formal C Memory Model Supporting Integer-Pointer Casts. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation(Portland, OR, USA)(PLDI ’15). Association for Computing Machinery, New York, NY, USA, 326–335. doi:10.1145/2737924.2738005

    work page doi:10.1145/2737924.2738005

  46. [46]

    Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi. 2018. Crellvm: Verified Credible Compilation for LLVM. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation(Philadelphia, PA, USA)(PLDI 2018). ...

    work page doi:10.1145/3192366.3192377 2018

  47. [47]

    Pierce, and Steve Zdancewic

    Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honor´e, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. InProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (Cascais, Portugal)(CPP 2019). ACM, Ne...

    work page doi:10.1145/3293880.3294106 2019

  48. [48]

    Ramana Kumar, Magnus O Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implemen- tation of ML.ACM SIGPLAN Notices49, 1 (2014), 179–191

    work page 2014

  49. [50]

    Xavier Leroy. 2009. Formal verification of a realistic compiler.Commun. ACM52, 7 (2009), 107–115. doi:10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  50. [51]

    Appel, Sandrine Blazy, and Gordon Stewart

    Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012.The CompCert Memory Model, Version 2. Research Report RR-7987. INRIA. 26 pages. https://hal.inria.fr/hal-00703441 HELIX: Verified compilation of cyber-physical control systems to LLVM IR 119

    work page 2012

  51. [53]

    Bell, Adam Chlipala, Benjamin C

    Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. 2022. C4: verified transactional objects.Proc. ACM Program. Lang.6, OOPSLA (2022), 1–31. doi:10.1145/3527324

    work page doi:10.1145/3527324 2022

  52. [54]

    Liyi Li and Elsa Gunter. 2020. K-LLVM: A Relatively Complete Semantics of LLVM IR. In34rd European Conference on Object-Oriented Programming, ECOOP 2020, Berlin, Germany. doi:10.4230/LIPIcs.ECOOP. 2020.7

    work page doi:10.4230/lipics.ecoop 2020

  53. [55]

    Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr

    Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded Translation Validation for LLVM. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation(Virtual, Canada)(PLDI 2021). Association for Computing Machinery, New York, NY, USA, 65–79. doi:10.1145/3453483.3454030

    work page doi:10.1145/3453483.3454030 2021

  54. [56]

    Tze-Meng Low and Franz Franchetti. 2017. High Assurance Code Generation for Cyber-Physical Systems. In IEEE International Symposium on High Assurance Systems Engineering (HASE)

    work page 2017

  55. [57]

    Vicente Macian, Jose Manuel Lujan, Carlos Guardiola, and Pedro Yuste. 2006. DFT-based controller for fuel injection unevenness correction in turbocharged diesel engines.IEEE transactions on control systems technology14, 5 (2006), 819–827

    work page 2006

  56. [58]

    Gregory Malecha. 2017. Speeding Up Proofs with Computational Reflection. https://gmalecha.github.io/ reflections/2017/speeding-up-proofs-with-computational-reflection. Accessed: 2020-09-01

    work page 2017

  57. [59]

    Gregory Malecha et al . 2012. ExtLib Coq library. https://github.com/coq-ext-lib/coq-ext-lib. Accessed: 2020-08-18

    work page 2012

  58. [60]

    Alvarez, and Sorin Lerner

    Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. 2016. Towards foundational verification of cyber-physical systems. In2016 Science of Security for Cyber-Physical Systems Workshop, SOSCYPS@CPSWeek 2016, Vienna, Austria, April 11, 2016. IEEE Computer Society, 1–5. doi:10.1109/ SOSCYPS.2016.7580000

    work page arXiv 2016

  59. [61]

    Appel, and Aleksey Nogin

    William Mansky, Andrew W. Appel, and Aleksey Nogin. 2017. A Verified Messaging System.Proc. ACM Program. Lang.1, OOPSLA, Article 87 (oct 2017), 28 pages. doi:10.1145/3133911

    work page doi:10.1145/3133911 2017

  60. [62]

    Mariano Moscato, Laura Titolo, Aaron Dutle, and C´esar A Munoz. 2017. Automatic estimation of verified floating-point round-off errors via static analysis. InComputer Safety, Reliability, and Security: 36th Inter- national Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings 36. Springer, 213–229

    work page 2017

  61. [63]

    Yiannis N Moschovakis. 1989. A mathematical modeling of pure, recursive algorithms. InInternational Symposium on Logical Foundations of Computer Science. Springer, 208–229

    work page 1989

  62. [64]

    Jos´e M. F. Moura, Jeremy Johnson, Robert W. Johnson, David Padua, Viktor K. Prasanna, Markus P¨ uschel, Bryan Singer, Manuela Veloso, and Jianxin Xiong. 2001. Generating Platform-Adapted DSP Libraries using SPIRAL. InHigh Performance Extreme Computing (HPEC)

    work page 2001

  63. [65]

    Scott Owens, Magnus O Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional big-step semantics. InEuropean Symposium on Programming. Springer, 589–615

    work page 2016

  64. [66]

    Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation validation. InTools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS’98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS’98 Lisbon, Portugal, March 28–April 4, 1998 Proceedings 4. Springer, 151–166

    work page 1998

  65. [67]

    P¨ uschel, J

    M. P¨ uschel, J. M. F. Moura, J. R. Johnson, D. Padua, M. M. Veloso, B. W. Singer, Jianxin Xiong, F. Franchetti, A. Gacic, Y. Voronenko, K. Chen, R. W. Johnson, and N. Rizzolo. 2005. SPIRAL: Code Generation for DSP Transforms.Proc. IEEE93, 2 (Feb 2005), 232–275. doi:10.1109/JPROC.2004.840306

    work page doi:10.1109/jproc.2004.840306 2005

  66. [68]

    Reynolds

    John C. Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. InProceedings of the ACM Annual Conference - Volume 2(Boston, Massachusetts, USA)(ACM ’72). Association for Computing Machinery, New York, NY, USA, 717–740. doi:10.1145/800194.805852

    work page doi:10.1145/800194.805852 1972

  67. [69]

    Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-Language Semantics and Verification. Proc. ACM Program. Lang.7, POPL, Article 27 (jan 2023), 31 pages. doi:10.1145/3571220

    work page doi:10.1145/3571220 2023

  68. [70]

    Jaroslav ˇSevˇc´ık, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2013. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.J. ACM60, 3 (2013), 22. doi:10. 120 Vadim Zaliva, Yannick Zakowski, Ilia Zaichuk, Valerii Huhnin, Calvin Beck, Irene Yoon, and Steve Zdancewic 1145/2487241.2487248

    work page arXiv 2013

  69. [71]

    Hirsch, and Steve Zdancewic

    Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. 2023b. Semantics for Noninterference with Interaction Trees. InProceedings of the 37th Annual European Conference on Object-Oriented Programming (ECOOP 2023)

    work page 2023

  70. [72]

    Lucas Silver, Eddy Westbrook, Matthew Yacavone, and Ryan Scott. 2023a. Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification. In37th European Conference on Object-Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim Ali ...

    work page doi:10.4230/lipics.ecoop.2023.30 2023

  71. [73]

    Lucas Silver and Steve Zdancewic. 2021. Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees.Proc. ACM Program. Lang.5, POPL, Article 26 (Jan. 2021), 28 pages. doi:10.1145/3434307

    work page doi:10.1145/3434307 2021

  72. [74]

    Alexey Solovyev, Marek S Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari ´c, and Ganesh Gopalakrishnan. 2018. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. ACM Transactions on Programming Languages and Systems (TOPLAS)41, 1 (2018), 1–39

    work page 2018

  73. [75]

    Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2019. CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification.Proc. ACM Program. Lang.4, POPL, Article 23 (Dec. 2019), 31 pages. doi:10.1145/3371091

    work page doi:10.1145/3371091 2019

  74. [76]

    Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement.Proc. ACM Program. Lang.7, POPL (2023), 1121–1151. doi:10.1145/ 3571232

    work page 2023

  75. [77]

    Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement.Proc. ACM Program. Lang.7, POPL, Article 39 (jan 2023), 31 pages. doi:10.1145/3571232

    work page doi:10.1145/3571232 2023

  76. [78]

    Matthieu Sozeau. 2010. A new look at generalized rewriting in type theory.Journal of Formalized Reasoning (2010), 1–12

    work page 2010

  77. [79]

    Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Th ´eo Winterhalter. 2020. The MetaCoq Project.Journal of Automated Reasoning(2020), 1–53

    work page 2020

  78. [80]

    Bas Spitters and Eelis Van der Weegen. 2011. Type classes for mathematics in type theory.Mathematical Structures in Computer Science21, 4 (2011), 795–825

    work page 2011

  79. [81]

    Michel Steuwer, Christian Fensch, Sam Lindley, and Christophe Dubach. 2015. Generating Performance Portable Code Using Rewrite Rules: From High-Level Functional Expressions to High-Performance OpenCL Code.SIGPLAN Not.50, 9 (Aug. 2015), 205–217. doi:10.1145/2858949.2784754

    work page doi:10.1145/2858949.2784754 2015

  80. [82]

    The GAP Group

    The GAP Group 2020.GAP – Groups, Algorithms, and Programming, Version 4.11.0. The GAP Group. https://www.gap-system.org

    work page 2020

Showing first 80 references.