1 citations · 1 across the 6 of their papers we have counts for
4 papers · 1 filter
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…
Schwarz: Solver-Aware Agentic Program Verification
Jingyu Ke, Ling-I Wu, Guoqiang Li
Agentic verification systems can often generate source-level specifications that look plausible, but plausibility is not enough: the verifier must still turn those specifications i…
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…
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…