Cover Image

K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zhao, Jianhong, Kang, Jinhui, Zhao, Yongwang
Format:	Preprint
Published:	2024
Subjects:	Software Engineering Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
by: Tempel, Sören, et al.
Published: (2024)

KBX: Verified Model Synchronization via Formal Bidirectional Transformation
by: Zhao, Jianhong, et al.
Published: (2024)

A Tool for Automated Reasoning About Traces Based on Configurable Formal Semantics
by: Erata, Ferhat, et al.
Published: (2024)

Container Morphisms for Composable Interactive Systems
by: Videla, André
Published: (2024)

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
by: Zhao, Jianhong, et al.
Published: (2025)

Shepherd: A Runtime Substrate Empowering Meta-Agents with a Formalized Execution Trace
by: Yu, Simon, et al.
Published: (2026)

KAIJU: An Executive Kernel for Intent-Gated Execution of LLM Agents
by: Guerin, Cormac, et al.
Published: (2026)

LEGO-Compiler: Enhancing Neural Compilation Through Translation Composability
by: Zhang, Shuoming, et al.
Published: (2025)

Teaching LLMs Program Semantics via Symbolic Execution Traces
by: Bayer, Jonas, et al.
Published: (2026)

FLAT: Formal Languages as Types
by: Zhu, Fengmin, et al.
Published: (2025)

CUTECat: Concolic Execution for Computational Law
by: Goutagny, Pierre, et al.
Published: (2024)

Multi-Pass Targeted Dynamic Symbolic Execution
by: Yavuz, Tuba
Published: (2024)

Python Symbolic Execution with LLM-powered Code Generation
by: Wang, Wenhan, et al.
Published: (2024)

Efficient Symbolic Execution of Software under Fault Attacks
by: Fang, Yuzhou, et al.
Published: (2025)

Zorya: Automated Concolic Execution of Single-Threaded Go Binaries
by: Gorna, Karolina, et al.
Published: (2025)

Package Managers à la Carte: A Formal Model of Dependency Resolution
by: Gibb, Ryan, et al.
Published: (2026)

Execution-Aware Program Reduction for WebAssembly via Record and Replay
by: Baek, Doehyun, et al.
Published: (2025)

Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
by: Saumya, Charitha, et al.
Published: (2023)

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
by: Bouras, Dimitrios Stamatios, et al.
Published: (2026)

PreciseBugCollector: Extensible, Executable and Precise Bug-fix Collection
by: Ye, He, et al.
Published: (2023)

Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection
by: Bhatia, Rishipal Singh
Published: (2026)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
by: Bucev, Mario, et al.
Published: (2024)

From a Natural to a Formal Language with DSL Assistant
by: Mosthaf, My M., et al.
Published: (2024)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
by: Le-Cong, Thanh, et al.
Published: (2025)

Can Large Language Models Simulate Symbolic Execution Output Like KLEE?
by: Feng, Rong, et al.
Published: (2025)

On Repairing Quantum Programs Using ChatGPT
by: Guo, Xiaoyu, et al.
Published: (2024)

An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization
by: Arfi, Farid, et al.
Published: (2024)

React-tRace: A Semantics for Understanding React Hooks
by: Lee, Jay, et al.
Published: (2025)

EnvTrace: Simulation-Based Semantic Evaluation of LLM Code via Execution Trace Alignment -- Demonstrated at Synchrotron Beamlines
by: van der Vleuten, Noah, et al.
Published: (2025)

Divergent Multi-Version Execution (DME): Canonical Instruction-Trace Fault Detection via Structural Address-Space Decorrelation
by: Yrievich, Petro Baran
Published: (2026)

Executing as You Generate: Hiding Execution Latency in LLM Code Generation
by: Sun, Zhensu, et al.
Published: (2026)

ARSP: Automated Repair of Verilog Designs via Semantic Partitioning
by: Yao, Bingkun, et al.
Published: (2025)

Hornet Node and the Hornet DSL: A Minimal, Executable Specification for Bitcoin Consensus
by: Sharp, Toby
Published: (2025)

The Argument for Meta-Modeling-Based Approaches to Hardware Generation Languages
by: Schreiner, Johannes, et al.
Published: (2024)

Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
by: Mitchell, Jacqueline L., et al.
Published: (2025)

Evaluating Program Semantics Reasoning with Type Inference in System F
by: He, Yifeng, et al.
Published: (2025)

Hardware.jl - An MLIR-based Julia HLS Flow (Work in Progress)
by: Short, Benedict, et al.
Published: (2025)

Semantic Source Code Segmentation using Small and Large Language Models
by: Dahou, Abdelhalim, et al.
Published: (2025)

CodeContests-O: Powering LLMs via Feedback-Driven Iterative Test Case Generation
by: Cai, Jianfeng, et al.
Published: (2026)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
by: Sanchez-Stern, Alex, et al.
Published: (2024)