Cover Image

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Paraskevopoulou, Zoe
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework
by: Izawa, Yusuke, et al.
Published: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
by: Jamner, Dustin, et al.
Published: (2025)

RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
by: Paraskevopoulou, Zoe, et al.
Published: (2024)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
by: Wu, Jinhua, et al.
Published: (2026)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
by: Rinard, Martin
Published: (2026)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

act: Technical report
by: Paraskevopoulou, Zoe, et al.
Published: (2026)

A Verified Compiler for Quantum Simulation
by: Li, Liyi, et al.
Published: (2025)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
by: Tekriwal, Mohit, et al.
Published: (2025)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
by: Conoly, Owen, et al.
Published: (2025)

Verifying Peephole Rewriting In SSA Compiler IRs
by: Bhat, Siddharth, et al.
Published: (2024)

Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations (Extended Version)
by: Qiu, Jie, et al.
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks
by: Zulkifli, Kahfi S., et al.
Published: (2025)

CompilerGPT: Leveraging Large Language Models for Analyzing and Acting on Compiler Optimization Reports
by: Pirkelbauer, Peter, et al.
Published: (2025)

Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams
by: Bolotina, Anna, et al.
Published: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

A Proof-Producing Compiler for Blockchain Applications
by: Avigad, Jeremy, et al.
Published: (2025)

Verified Parameterized Choreographies Technical Report
by: Rubbens, Robert, et al.
Published: (2025)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
by: Thibault, Jérémy, et al.
Published: (2025)

Compilation of Modular and General Sparse Workspaces
by: Zhang, Genghan, et al.
Published: (2024)

Foundational Verification of Smart Contracts through Verified Compilation
by: Sjöberg, Vilhelm, et al.
Published: (2024)

depyf: Open the Opaque Box of PyTorch Compiler for Machine Learning Researchers
by: You, Kaichao, et al.
Published: (2024)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

CompilerDream: Learning a Compiler World Model for General Code Optimization
by: Deng, Chaoyi, et al.
Published: (2024)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
by: Gross, Jason, et al.
Published: (2022)

Is It a Good Idea to Build an HLS Tool on Top of MLIR? Experience from Building the Dynamatic HLS Compiler
by: Xu, Jiahui, et al.
Published: (2026)

The CoCompiler: DSL Lifting via Relational Compilation
by: Spargo, Naomi, et al.
Published: (2025)

Compiling with Arrays
by: Richter, David, et al.
Published: (2024)

TENSURE: Fuzzing Sparse Tensor Compilers (Registered Report)
by: Mahathevan, Kabilan, et al.
Published: (2026)

Bounded Exhaustive Random Program Generation for Testing Solidity Compilers
by: Ma, Haoyang, et al.
Published: (2025)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Generating Compilers for Qubit Mapping and Routing
by: Molavi, Abtin, et al.
Published: (2025)

Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
by: Rinard, Martin
Published: (2026)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
by: Foo, Darius, et al.
Published: (2023)

Can Proof Assistants Verify Multi-Agent Systems?
by: Mendez, Julian Alfredo, et al.
Published: (2025)

CrypTorch: PyTorch-based Auto-tuning Compiler for Machine Learning with Multi-party Computation
by: Liu, Jinyu, et al.
Published: (2025)

Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
by: Halftermeyer, Pierre
Published: (2026)

Axe: A Simple Unified Layout Abstraction for Machine Learning Compilers
by: Hou, Bohan, et al.
Published: (2026)

E-Graphs as a Persistent Compiler Abstraction
by: Merckx, Jules, et al.
Published: (2026)