2 papers
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…