Buchumschlag

Verifying Peephole Rewriting In SSA Compiler IRs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Bhat, Siddharth, Keizer, Alex, Hughes, Chris, Goens, Andrés, Grosser, Tobias
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Programming Languages Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
von: Monniaux, David
Veröffentlicht: (2024)

Linearization via Rewriting (Long Version)
von: Lago, Ugo Dal, et al.
Veröffentlicht: (2025)

On Complexity Bounds and Confluence of Parallel Term Rewriting
von: Baudon, Thaïs, et al.
Veröffentlicht: (2023)

Confluence of Conditional Rewriting Modulo
von: Lucas, Salvador
Veröffentlicht: (2025)

Verifying Floating-Point Programs in Stainless
von: Gilot, Andrea, et al.
Veröffentlicht: (2026)

Verifying Lock-free Search Structure Templates
von: Patel, Nisarg, et al.
Veröffentlicht: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
von: Murphy, Charlie, et al.
Veröffentlicht: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
von: Paganoni, Marco, et al.
Veröffentlicht: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
von: Wang, Keyin, et al.
Veröffentlicht: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
von: Coglio, Alessandro, et al.
Veröffentlicht: (2025)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
von: de Vilhena, Paulo Emílio, et al.
Veröffentlicht: (2021)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
von: Grandury, Marcos, et al.
Veröffentlicht: (2025)

A Proof-Producing Compiler for Blockchain Applications
von: Avigad, Jeremy, et al.
Veröffentlicht: (2025)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
von: Kappé, Tobias, et al.
Veröffentlicht: (2023)

Finite-Choice Logic Programming
von: Martens, Chris, et al.
Veröffentlicht: (2024)

Substructural Parametricity
von: Aberlé, C. B., et al.
Veröffentlicht: (2025)

Verifying Asynchronous Hyperproperties in Reactive Systems
von: Beutner, Raven, et al.
Veröffentlicht: (2025)

Functional Array Programming in an Extended Pi-Calculus
von: Hüttel, Hans, et al.
Veröffentlicht: (2024)

Quantum Circuits Are Just a Phase
von: Heunen, Chris, et al.
Veröffentlicht: (2025)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
von: Batz, Kevin, et al.
Veröffentlicht: (2024)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
von: Batz, Kevin, et al.
Veröffentlicht: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
von: Li, Guchan, et al.
Veröffentlicht: (2026)

Flexible Correct-by-Construction Programming
von: Runge, Tobias, et al.
Veröffentlicht: (2022)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
von: Ileri, Atalay Mert, et al.
Veröffentlicht: (2024)

The Denotational Semantics of SSA
von: Ghalayini, Jad Elkhaleq, et al.
Veröffentlicht: (2024)

Verified Purely Functional Catenable Real-Time Deques
von: Viennot, Jules, et al.
Veröffentlicht: (2025)

Kleene algebra with commutativity conditions is undecidable
von: de Amorim, Arthur Azevedo, et al.
Veröffentlicht: (2024)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
von: Yubeaton, Patrick, et al.
Veröffentlicht: (2025)

Tunable Automation in Automated Program Verification
von: Bai, Alexander Y., et al.
Veröffentlicht: (2025)

Can Proof Assistants Verify Multi-Agent Systems?
von: Mendez, Julian Alfredo, et al.
Veröffentlicht: (2025)

Verified VCG and Verified Compiler for Dafny
von: Nezamabadi, Daniel, et al.
Veröffentlicht: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
von: Kaye, George
Veröffentlicht: (2025)

Impredicativity in Linear Dependent Type Theory
von: Speight, Sam, et al.
Veröffentlicht: (2026)

Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
von: Fan, Wen, et al.
Veröffentlicht: (2024)

Structural Temporal Logic for Mechanized Program Verification
von: Ioannidis, Eleftherios, et al.
Veröffentlicht: (2024)

An Introduction to Different Approaches to Initial Semantics
von: Lamiaux, Thomas, et al.
Veröffentlicht: (2024)

More Church-Rosser Proofs in BELUGA
von: Momigliano, Alberto, et al.
Veröffentlicht: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
von: Goncharov, Sergey, et al.
Veröffentlicht: (2024)

A Nominal Approach to Probabilistic Separation Logic
von: Li, John M., et al.
Veröffentlicht: (2024)