EDBT 2026 Demo / reviewers in the wild / expert
Zhongsheng Zhan
dblp:425/5321
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2026
0009-0004-7151-9608ORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Computer architecture, parallel and distributed computing, and storage systems
1 paper |
Electronic design automation · 87% Distributed systems · 13% | |
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 100% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Programming languages and type systems › language semantics
core calculus |
1.0 | 1 | 2026 | ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026 |
Programming languages and type systems
language design |
1.0 | 1 | 2026 | ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026 |
Electronic design automation
hardware verification and test |
1.0 | 1 | 2026 | ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026 |
Electronic design automation › hardware verification and test
static analysis |
1.0 | 1 | 2026 | ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026 |
Distributed systems
bug detection |
0.3 | 1 | 2026 | ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026 |
Methods — techniques the papers use, named apart from their topics
fixed-point analysis · 2.0logical relations · 1.0logical relation · 1.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | ChiSA: Static Analysis for Lightweight Chisel VerificationabstractThe growing demand for productivity in hardware development opens up new opportunities for applying programming language (PL) techniques to hardware description languages (HDLs). Chisel, a leading agile HDL, embraces this shift by leveraging modern PL features to enhance hardware design productivity. However, verification for Chisel remains a major productivity bottleneck, requiring substantial time and manual effort. To address this issue, we advocate the use of static analysis —a technique proven well-suited to agile development workflows in software—for lightweight Chisel verification. This work establishes a theoretical foundation for Chisel static analysis. At its core is λ C , a formal core calculus of ChAIR (a Chisel-specific intermediate representation for analysis). λ C is the first formalism that captures the essence of Chisel while being deliberately minimal to ease rigorous reasoning about static analysis built on λ C . We prove key properties of λ C that reflect real hardware characteristics, which in turn offer a form of retrospective validation for its design. On the basis of λ C , we define and formalize the hardware value flow analysis (HVFA) problem, which underpins our static analyses for critical Chisel verification tasks, including bug detection and security analysis. We then propose a synchronized fixed-point solution to the HVFA problem, featuring hardware-specific treatment of the synchronous behavior of clock-driven hardware registers—the essential feature of Chisel programs. We further prove key theorems establishing the guarantees and limitations of our solution. As a proof of concept, we develop ChiSA (30K+ LoC)—the first Chisel static analyzer that can analyze intricate hardware value flows to enable lightweight analyses for critical Chisel verification tasks such as bug detection and security analysis. To facilitate thorough evaluation of both ChiSA and future work, we provide ChiSABench (11M+ LoC), a comprehensive benchmark for Chisel static analysis. Our evaluation on ChiSABench demonstrates that ChiSA offers an effective and significantly more lightweight approach for critical Chisel verification tasks, especially on large and complex real-world designs. For example, ChiSA identified 69 violable developer-inserted assertions in large-scale Chisel designs (9.7M+ LoC) in under 200 seconds—eight of which were recognized by developers and scheduled for future fixes—and detected all 60 information-leak vulnerabilities in the well-known TrustHub benchmark (1.1M+ LoC) in just one second—outperforming state-of-the-art Chisel approaches like ChiselTest’s bounded model checking and ChiselFlow’s secure type system. These results underscore the high promise of static analysis for lightweight Chisel verification. To encourage continued research and innovation, we will fully open-source ChiSA (30K+ LoC) and ChiSABench (11M+ LoC). Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan 0001, Yue Li 0006 |
Proc. ACM Program. Lang. | 3 |