Demo Data from SIGIR 2026 / reviewers in the wild / expert
Denghang Hu
dblp:270/1543
· DBLP profile ↗
7ranked-venue papers
3as first author
6since 2021 · last 2025
0009-0004-6928-6032ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 5 · 1 first-author · 4 since 2021Theory of computation · 2 · 1 first-author · 2 since 2021Systems, architecture and hardware · 1 · 1 first-author · 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 · 87% Programming languages and type systems · 13% | |
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 50% Automata and formal languages · 50% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis › constraint solving
string constraint solving |
0.6 | 1 | 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variables · Proc. ACM Program. Lang. 2022 |
Program analysis
symbolic execution |
0.6 | 1 | 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variables · Proc. ACM Program. Lang. 2022 |
Automated reasoning and model checking › constraint solving
string constraint solving |
0.6 | 1 | 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variables · Proc. ACM Program. Lang. 2022 |
Automata and formal languages
transducers |
0.6 | 1 | 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variables · Proc. ACM Program. Lang. 2022 |
Programming languages and type systems › language semantics
regular expression semantics |
0.2 | 1 | 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variables · Proc. ACM Program. Lang. 2022 |
Methods — techniques the papers use, named apart from their topics
sequent calculus · 1.1pre-image and post-image computation · 1.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Decision Procedure for a Theory of String Sequences
Denghang Hu, Taolue Chen 0001, Philipp Rümmer, Fu Song, Zhilin Wu |
APLAS | 1 |
| 2025 | OSTRICH2: Solver for Complex String Constraints
Matthew Hague, Denghang Hu, Artur Jez, Anthony Widjaja Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu |
FMCAD | 2 |
| 2025 | An efficient string solver for string constraints with regex-counting and string-length
Denghang Hu, Zhilin Wu |
J. Syst. Archit. | 1 |
| 2023 | String Constraints with Regex-Counting and String-Length Solved More Efficiently
Denghang Hu, Zhilin Wu |
SETTA | 1 |
| 2022 | Solving string constraints with Regex-dependent functions through transducers with priorities and variablesabstractRegular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency. Taolue Chen 0001, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu |
Proc. ACM Program. Lang. | 5 |
| 2021 | Solving Not-Substring Constraint withFlat Abstraction
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen 0001, Bui Phi Diep, Lukás Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen |
APLAS | 6 |
| 2020 | A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Taolue Chen 0001, Matthew Hague, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu |
ATVA | 4 |