EDBT 2026 Demo / reviewers in the wild / expert
Xiaokai Rong
dblp:409/1243
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
—ORCID · unresolved
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Program analysis · 67% Program verification · 33% | |
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 100% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis
constraint solving |
0.9 | 1 | 2025 | Large Language Models for Safe Minimization · ICSE 2025 |
Program analysis › control flow analysis
infeasible path detection |
0.9 | 1 | 2025 | Large Language Models for Safe Minimization · ICSE 2025 |
Program verification › decision procedure
satisfiability modulo theories |
0.9 | 1 | 2025 | Large Language Models for Safe Minimization · ICSE 2025 |
Automated reasoning and model checking › constraint solving
string constraint solving |
0.3 | 1 | 2025 | Large Language Models for Safe Minimization · ICSE 2025 |
Methods — techniques the papers use, named apart from their topics
sample-and-enumerate decoding · 1.7large language model · 1.7SMT solvers · 0.9SMT solver · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Large Language Models for Safe MinimizationabstractSeveral tasks in program analysis, verification, and testing are modeled as constraint solving problems, utilizing SMT solvers as the reasoning engine. In this work, we aim to investigate the reasoning capabilities of large language models (LLMs) toward reducing the size of an infeasible string constraint system by exploiting inter-constraint interactions such that the remaining ones are still unsatisfiable. We term this safe minimization. Motivated by preliminary observations of hallucination and error propagation in LLMs, we design SafeMin, a framework leveraging an LLM and SMT solver in tandem to ensure a safe and correct minimization. We test the applicability of our approach on string benchmarks from LeetCode in the computation of minimal unsatisfiable subsets (MUSes). We observed that SafeMin helps safely minimize 94.3% of these constraints, with an average minimization ratio of 98% relative to the MUSes. In addition, we assess SafeMin's capabilities in partially enumerating non-unique MUSes, which is baked into our approach via a “sample-and-enumerate” decoding strategy. Overall, we captured 42.1% more non-unique MUSes than without such LLM-based macro-reasoning. Finally, we demonstrate SafeMin's usefulness in detecting infeasible paths in programs. Aashish Yadavally, Xiaokai Rong, Phat Nguyen, Tien N. Nguyen |
ICSE | 2 |