I am interested in the co-design of formal analysis and AI agents for reliable and efficient reasoning. My work explores two complementary directions: making rigorous analysis practical for interactive agent workloads, and making agent tasks amenable to derivation, checking, and constraint solving.
SPONGE studies efficient online value-flow analysis. My recent work, ReCoNav, formalizes constrained long-horizon navigation so that decisions supported by grounded premises can be derived and checked, while LLMs and VLMs handle unresolved semantics.
I welcome research collaborations and internship opportunities in these areas.
@article{peng2026sponge,
title = {SPONGE: Adaptive Boundary-Anchored Indexing
for Online Value-Flow Queries},
author = {Peng, Sixiang and Sun, Chenyang and Chen, Wei
and Zhang, Bowen and Zhang, Charles},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
articleno = {340},
year = {2026},
doi = {10.1145/3839472}
}
The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries.
Manuscripts
ReCoNav: Reliable Constrained Long-Horizon Vision-and-Language Navigation via a Determination Engine
Manuscript under review·2026
KeywordsVision-and-language navigation; task contracts; constraint reasoning; grounding; planning and verification
Abstract
Conventional vision-and-language navigation (VLN) asks an agent to follow a described route to a destination. Practical missions can require multiple ordered visits, with hard constraints and preferences governing both target selection and connecting routes. Existing agents use memories, maps, or constraint-guided planning, but reliably propagating scoped requirements across interpretation, grounding, and complete-route planning remains challenging. We introduce ReCoNav, whose instruction contract models route requirements for joint target and route selection. Its Determination Engine uses scene and task rules to propagate route constraints across interpretation, grounding, and planning. Derived evidence determines choices, verifies judgments, and guides repair; vision-language models supply unresolved semantics. We construct a benchmark of 192 scene-grounded tasks across nine indoor scenes to evaluate joint target and route satisfaction. Existing methods show low satisfaction and frequent timeouts. On 44 constraint-resolving tasks without the added time limit, global scene access helps but remains insufficient: ReCoNav achieves 81.82% full instruction satisfaction, versus 29.55% for the best evaluated existing method given global scene information and 38.64% for direct planning with feedback sharing our scene information, backbone, and solver. Across four backbones, ReCoNav improves satisfaction with fewer model tokens than this feedback baseline; ablations support explicit contract-based planning, global determination, and verification with repair.