Cover Image

Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kan, Shuanglong, Ertel, Sebastian
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

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

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

A Multi-level Compiler Backend for Accelerated Micro-kernels Targeting RISC-V ISA Extensions
by: Lopoukhine, Alexandre, et al.
Published: (2025)

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

Zoozve: A Strip-Mining-Free RISC-V Vector Extension with Arbitrary Register Grouping Compilation Support (WIP)
by: Xu, Siyi, et al.
Published: (2025)

Compilation as Multi-Language Semantics
by: Bowman, William J.
Published: (2025)

Generation of Compiler Backends from Formal Models of Hardware
by: Smith, Gus Henry
Published: (2024)

CIR+CVN: Bridging LLM Semantic Understanding and Petri-Net Verification for Concurrent Programs
by: Zhang, Kaiwen, et al.
Published: (2026)

Compilation Semantics for a Programming Language with Versions
by: Tanabe, Yudai, et al.
Published: (2023)

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

Verification of the Release-Acquire Semantics
by: Abdulla, Parosh, et al.
Published: (2025)

A Compiler for Operations on Relations with Bag Semantics
by: Dong, James, et al.
Published: (2025)

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
by: Zhao, Jianhong, 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)

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
by: Nagar, Kartik, et al.
Published: (2020)

Linguine: A Natural-Language Programming Language with Formal Semantics and a Clean Compiler Pipeline
by: Hu, Lifan
Published: (2025)

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

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

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

QCoder Benchmark: Bridging Language Generation and Quantum Hardware through Simulator-Based Feedback
by: Mikuriya, Taku, et al.
Published: (2025)

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

Compiling Gradual Types with Evidence
by: Romero, José Luis, et al.
Published: (2025)

Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
by: Daggitt, Matthew L., et al.
Published: (2026)

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

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

Partial Evaluation, Whole-Program Compilation
by: Fallin, Chris, et al.
Published: (2024)

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

An Optimizing Just-In-Time Compiler for Rotor
by: Trindade, João H., et al.
Published: (2024)

From CISC to RISC: language-model guided assembly transpilation
by: Heakl, Ahmed, et al.
Published: (2024)

K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
by: Zhao, Jianhong, et al.
Published: (2024)

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

Bonsai: Compiling Queries to Pruned Tree Traversals
by: Root, Alexander J, et al.
Published: (2025)

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

Prime Path Coverage in the GNU Compiler Collection
by: Kvalsvik, Jørgen
Published: (2025)

Cyclotron: Compilation of Recurrences to Distributed and Systolic Architectures
by: Sundram, Shiv, et al.
Published: (2025)

Macro-embedding Compiler Intermediate Languages in Racket
by: Bowman, William J.
Published: (2025)

Compiling the Mimosa programming language to RTOS tasks
by: Huber, Nikolaus, et al.
Published: (2025)

Meta-compilation of Baseline JIT Compilers with Druid
by: Palumbo, Nahuel, et al.
Published: (2025)

Scaling Optimization Over Uncertainty via Compilation
by: Cho, Minsung, et al.
Published: (2025)

Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset
by: Menon, Anand, et al.
Published: (2025)