Buchumschlag

Practical Formal Verification for MLIR Programs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Tucker, Emily, Pouchet, Louis-Noël, Hunhoff, Erika, Neuendorffer, Stephen, Wang, Erwei
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

A Unified Framework for Automated Code Transformation and Pragma Insertion
von: Pouget, Stéphane, et al.
Veröffentlicht: (2024)

From Loop Nests to Silicon: Mapping AI Workloads onto AMD NPUs with MLIR-AIR
von: Wang, Erwei, et al.
Veröffentlicht: (2025)

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
von: Peng, Xuanyu, et al.
Veröffentlicht: (2025)

Efficient Formal Verification of Quantum Error Correcting Programs
von: Huang, Qifan, et al.
Veröffentlicht: (2025)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
von: Dane, Serra Z., et al.
Veröffentlicht: (2026)

Building Bridges: Julia as an MLIR Frontend
von: Merckx, Jules
Veröffentlicht: (2025)

MLIR-Smith: A Novel Random Program Generator for Evaluating Compiler Pipelines
von: Ates, Berke, et al.
Veröffentlicht: (2026)

MLIR-Forge: A Modular Framework for Language Smiths
von: Ates, Berke, et al.
Veröffentlicht: (2026)

WAMI: Compilation to WebAssembly through MLIR without Losing Abstraction
von: Kang, Byeongjee, et al.
Veröffentlicht: (2025)

Data Transfer Optimizations for Host-CPU and Accelerators in AXI4MLIR
von: Haris, Jude, et al.
Veröffentlicht: (2024)

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

The MLIR Transform Dialect. Your compiler is more powerful than you think
von: Lücke, Martin Paul, et al.
Veröffentlicht: (2024)

An Optimizing Framework on MLIR for Efficient FPGA-based Accelerator Generation
von: Zhang, Weichuang, et al.
Veröffentlicht: (2024)

Demonstrating a Future for MLIR-native DSL Compilers on a NumPy-like Example
von: Friebel, Karl F. A., et al.
Veröffentlicht: (2026)

Analyzing Latency Hiding and Parallelism in an MLIR-based AI Kernel Compiler
von: Absar, Javed, et al.
Veröffentlicht: (2026)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
von: Hansen, Zachary
Veröffentlicht: (2025)

QCP: A Practical Separation Logic-based C Program Verification Tool
von: Wu, Xiwei, et al.
Veröffentlicht: (2025)

Fully integrating the Flang Fortran compiler with standard MLIR
von: Brown, Nick
Veröffentlicht: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
von: Kasibatla, Saketh Ram, et al.
Veröffentlicht: (2024)

Hexagon-MLIR: An AI Compilation Stack For Qualcomm's Neural Processing Units (NPUs)
von: Absar, Mohammed Javed, et al.
Veröffentlicht: (2026)

An MLIR Lowering Pipeline for Stencils at Wafer-Scale
von: Stawinoga, Nicolai, et al.
Veröffentlicht: (2026)

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

An MLIR pipeline for offloading Fortran to FPGAs via OpenMP
von: Rodriguez-Canal, Gabriel, et al.
Veröffentlicht: (2025)

Formal Verification of Variational Quantum Circuits
von: Assolini, Nicola, et al.
Veröffentlicht: (2025)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
von: Councilman, Aaron, et al.
Veröffentlicht: (2025)

Solvable Tuple Patterns and Their Applications to Program Verification
von: Kobayashi, Naoki, et al.
Veröffentlicht: (2025)

C*: Unifying Programming and Verification in C
von: Cao, Yiyuan, et al.
Veröffentlicht: (2025)

Hardware.jl - An MLIR-based Julia HLS Flow (Work in Progress)
von: Short, Benedict, et al.
Veröffentlicht: (2025)

VyZX: Formal Verification of a Graphical Quantum Language
von: Lehmann, Adrian, et al.
Veröffentlicht: (2023)

Automated Formal Verification of a Software Fault Isolation System
von: Sotoudeh, Matthew, et al.
Veröffentlicht: (2025)

From Algebraic Word Problem to Program: A Formalized Approach
von: Wiemerslage, Adam, et al.
Veröffentlicht: (2020)

Towards Automated Verification of LLM-Synthesized C Programs
von: Mukherjee, Prasita, et al.
Veröffentlicht: (2024)

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

Minuska: Towards a Formally Verified Programming Language Framework
von: Tušil, Jan, et al.
Veröffentlicht: (2024)

Formal Simulation and Visualisation of Hybrid Programs
von: Mendes, Pedro, et al.
Veröffentlicht: (2024)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
von: Barrière, Aurèle, et al.
Veröffentlicht: (2025)

VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
von: Xin, Yutong, et al.
Veröffentlicht: (2026)

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
von: Bagrel, Thomas
Veröffentlicht: (2026)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
von: Chang, Fu-Chieh, et al.
Veröffentlicht: (2026)

Analyzing LLM Instruction Optimization for Tabular Fact Verification
von: Du, Xiaotang, et al.
Veröffentlicht: (2026)