4 papers
Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction
Xi Yang, Taolue Chen, Yuqi Chen +3
Fault injection attacks deliberately inject faults into a device via physical channels to disturb its regular execution. Adversaries can effectively deduce secrets by analyzing bot…
Can LLM Aid in Solving Constraints with Inductive Definitions?
Weizhi Feng, Shidong Shen, Jiaxiang Liu +3
Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for…
A Formally Verified Procedure for Width Inference in FIRRTL
Keyin Wang, Xiaomu Shi, Jiaxiang Liu +4
FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of many components are not specified explic…
Decision Procedure for A Theory of String Sequences
Denghang Hu, Taolue Chen, Philipp Rümmer +2
The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and pr…