3 papers
cs.PL2026
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Jingyu Ke, Jingyang Li, Guoqiang Li
Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measure…
cs.DB2026
Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance
Jingyu Ke, Jingyang Li, Guoqiang Li
SQL rewrite verification must account for duplicate rows, observable row order, and typed value semantics. Existing verifiers have yet to combine proofs over database instances of…
cs.PL2026
Array-Carrying Symbolic Execution for Function Contract Generation
Weijie Lu, Jingyu Ke, Hongfei Fu +4
Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is funda…