Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.
Title resolution pending
11 Pith papers cite this work. Polarity classification is still indexing.
11
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
roles
background 2representative citing papers
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
Matroid certificates from coordinate ranks bound zero-error confusability capacity; realizable relations are upward-closed agreement families, with host realizability equivalent to zero-delay synchronization plus side information.
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
WybeCoder interleaves code generation, invariant synthesis, and proof construction to produce verified imperative programs, solving 74% of Verina tasks and 62% of Clever tasks while surpassing prior results.
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.
Human-Certified Module Repositories (HCMRs) are proposed as a new architectural model blending human oversight with automated analysis to certify reusable software modules for safe assembly by humans and AI agents.
Describes integrating symbolic code reasoning into CS1 and discrete math courses at Haverford and Grinnell, introduces the Orca proof assistant, and poses research questions on effectiveness.
Authors describe designing a compiler course that uses Why3 to teach certified compilation, leading to a verified simple imperative language compiler, along with student and teacher evaluations.
citing papers explorer
-
Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.
-
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
-
Zero-Error Recovery under Deterministic Partial Views: Matroid Bounds and Verifiable Realizability
Matroid certificates from coordinate ranks bound zero-error confusability capacity; realizable relations are upward-closed agreement families, with host realizability equivalent to zero-delay synchronization plus side information.
-
Understanding GCC Builtins to Develop Better Tools
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
-
WybeCoder: Verified Imperative Code Generation
WybeCoder interleaves code generation, invariant synthesis, and proof construction to produce verified imperative programs, solving 74% of Verina tasks and 62% of Clever tasks while surpassing prior results.
-
On Reasoning-Centric LLM-based Automated Theorem Proving
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.
-
Human-Certified Module Repositories for the AI Age
Human-Certified Module Repositories (HCMRs) are proposed as a new architectural model blending human oversight with automated analysis to certify reusable software modules for safe assembly by humans and AI agents.
-
A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete Math
Describes integrating symbolic code reasoning into CS1 and discrete math courses at Haverford and Grinnell, introduces the Orca proof assistant, and poses research questions on effectiveness.
-
Introducing Certified Compilation in Education by a Functional Language Approach
Authors describe designing a compiler course that uses Why3 to teach certified compilation, leading to a verified simple imperative language compiler, along with student and teacher evaluations.
- Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
- Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries