2 citations · 3 across the 3 of their papers we have counts for
3 papers
Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
Jianhong Zhao, Everett Hildenbrandt, Juan Conejero +1
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into…
KBX: Verified Model Synchronization via Formal Bidirectional Transformation
Jianhong Zhao, Yongwang Zhao, Peisen Yao +3
Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformati…
K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
Jianhong Zhao, Jinhui Kang, Yongwang Zhao
CIRCT, an open-source EDA framework akin to LLVM for software, is a foundation for various hardware description languages. Despite its crucial role, CIRCT's lack of formal semantic…