4 papers
SimP: Unifying Syntax- and Semantic-Guided Techniques for Efficient Program Reduction
Ye Xiong, Xiangyu Gao, Qiaochu Chen +2
Compiler bugs are pervasive in modern compiler systems, but the test programs that trigger them are often too large for practical debugging. Program reduction addresses this by min…
CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation
Anirudh Khatry, Robert Zhang, Jia Pan +4
C-to-Rust transpilation is essential for modernizing legacy C code while enhancing safety and interoperability with modern Rust ecosystems. However, no dataset currently exists for…
Active Learning for Neurosymbolic Program Synthesis
Celeste Barnaby, Qiaochu Chen, Ramya Ramalingam +2
The goal of active learning for program synthesis is to synthesize the desired program by asking targeted questions that minimize user interaction. While prior work has explored ac…
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin, Jimmy Xin, Gabriel Poesia +3
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-st…