Cover Image

A Formally Verified Procedure for Width Inference in FIRRTL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wang, Keyin, Shi, Xiaomu, Liu, Jiaxiang, Wu, Zhilin, Chen, Taolve, Song, Fu, Jansen, David N.
Format:	Preprint
Published:	2026
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
by: Ileri, Atalay Mert, et al.
Published: (2024)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
by: Zhang, Cheng, et al.
Published: (2026)

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

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
by: Murphy, Charlie, et al.
Published: (2024)

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

Verifying Functional Correctness Properties At the Level of Java Bytecode
by: Paganoni, Marco, et al.
Published: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

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

A Graded Modal Dependent Type Theory with Erasure, Formalized
by: Abel, Andreas, et al.
Published: (2026)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
by: Lee, Jaeseo, et al.
Published: (2025)

Equational Bit-Vector Solving via Strong Gröbner Bases
by: Song, Jiaxin, et al.
Published: (2024)

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

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
by: Agarwal, Shubham, et al.
Published: (2026)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
by: Thakur, Amitayush, et al.
Published: (2025)

Verifying Asynchronous Hyperproperties in Reactive Systems
by: Beutner, Raven, et al.
Published: (2025)

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

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

Four Formal Models of IEEE 1394 Link Layer
by: Garavel, Hubert, et al.
Published: (2024)

Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems
by: Lang, Frédéric, et al.
Published: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
by: Kasibatla, Saketh Ram, et al.
Published: (2024)

Proceedings 9th edition of Working Formal Methods Symposium
by: Arusoaie, Andrei, et al.
Published: (2025)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
by: Hansen, Zachary
Published: (2025)

Verified Purely Functional Catenable Real-Time Deques
by: Viennot, Jules, et al.
Published: (2025)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
by: Yubeaton, Patrick, et al.
Published: (2025)

Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
by: Garavel, Hubert
Published: (2026)

Can LLM Aid in Solving Constraints with Inductive Definitions?
by: Feng, Weizhi, et al.
Published: (2026)

Positive Focusing is Directly Useful
by: Accattoli, Beniamino, et al.
Published: (2024)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Pleasant Imperative Program Proofs with GallinaC
by: Fort, Frédéric, et al.
Published: (2025)

VERINA: Benchmarking Verifiable Code Generation
by: Ye, Zhe, et al.
Published: (2025)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

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

Provenance Guided Rollback Suggestions
by: Zhao, David, et al.
Published: (2025)