1 citations · 1 across the 6 of their papers we have counts for
7 papers
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…
Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
Ruibang Liu, Minyu Chen, Ling-I Wu +2
Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, t…
Piecewise Analysis of Probabilistic Programs via -Induction
Tengshun Yang, Shenghua Feng, Hongfei Fu +3
In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most pr…
Affine Disjunctive Invariant Generation with Farkas' Lemma
Jingyu Ke, Hongfei Fu, Hongming Liu +3
In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approac…