Cover Image

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wu, Jinhua, Wang, Yuting, Yu, Liukun, Meng, Linglong
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

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

Denotation-based Compositional Compiler Verification
by: Cheng, Zhang, et al.
Published: (2024)

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

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

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

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

Qafny: A Quantum-Program Verifier
by: Li, Liyi, et al.
Published: (2022)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
by: Paraskevopoulou, Zoe
Published: (2026)

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

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

Dependent Session Types for Verified Concurrent Programming
by: Fu, Qiancheng, et al.
Published: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
by: Schröer, Philipp, et al.
Published: (2026)

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

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
by: Shen, Gan, et al.
Published: (2024)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
by: Yang, Xiaoxiao, et al.
Published: (2017)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
by: Fedchin, Aleksandr, et al.
Published: (2025)

Verified Code Transpilation with LLMs
by: Bhatia, Sahil, et al.
Published: (2024)

LoRe: A Programming Model for Verifiably Safe Local-First Software
by: Haas, Julian, et al.
Published: (2023)

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

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
by: Pezeshkpour, Pouya, et al.
Published: (2026)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

Certified Program Synthesis with a Multi-Modal Verifier
by: Feng, Yueyang, et al.
Published: (2026)

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

Increasing the Expressiveness of a Gradual Verifier
by: Gupta, Priyam
Published: (2025)

Automatically Verifying Replication-aware Linearizability
by: Soundarapandian, Vimala, et al.
Published: (2025)

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

Verifying Sequential Consistency under Bounded Preemptions
by: Govind, R., et al.
Published: (2026)

Verifying Fault-Tolerance of Quantum Error Correction Codes
by: Chen, Kean, et al.
Published: (2025)

Crux, a Precise Verifier for Rust and Other Languages
by: Pernsteiner, Stuart, et al.
Published: (2024)

KATch: A Fast Symbolic Verifier for NetKAT
by: Moeller, Mark, et al.
Published: (2024)

Formally Verified Linear-Time Invertible Lexing
by: Chassot, Samuel, et al.
Published: (2025)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Faster Verified Explanations for Neural Networks
by: De Palma, Alessandro, et al.
Published: (2025)