hengxin.github.io/publications.html at master · hengxin/hengxin.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
  "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
<head>
<meta name="generator" content="jemdoc, see http://jemdoc.jaboc.net/" />
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link rel="stylesheet" href="jemdoc.css" type="text/css" />
<title>Hengfeng Wei (éæ’å³°)</title>
</head>
<body>
<table summary="Table for page layout." id="tlayout">
<tr valign="top">
<td id="layout-menu">
<div class="menu-category">menu</div>
<div class="menu-item"><a href="index.html">Home</a></div>
<div class="menu-item"><a href="teaching.html">Teaching</a></div>
<div class="menu-item"><a href="research.html">Research</a></div>
<div class="menu-item"><a href="publications.html" class="current">Publications</a></div>
<div class="menu-item"><a href="awards.html">Awards</a></div>
<div class="menu-item"><a href="activities.html">Activities</a></div>
<div class="menu-category">group</div>
<div class="menu-item"><a href="students.html">Students</a></div>
<div class="menu-item"><a href="enrollment.html">Enrollment</a></div>
<div class="menu-item"><a href="contact.html">Contact</a></div>
<div class="menu-category">links</div>
<div class="menu-item"><a href="ocw.html">OCW</a></div>
<div class="menu-item"><a href="social.html">Social</a></div>
</td>
<td id="layout-content">
<div id="toptitle">
<h1>Hengfeng Wei (éæ’å³°)</h1>
</div>
<div class="infoblock">
<div class="blockcontent">
<p><b>(*: Corresponding Author)</b></p>
<h4>2025</h4>
<ol>
<li><p>Weining Cao, Guangyuan Wu, Tangzhi Xu, Yuan Yao, <b>Hengfeng Wei</b>, Taolue Chen, Xiaoxing Ma.<br />
<i>Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference</i>.<br />
Proc. ACM Softw. Eng., Vol. 2, No. ISSTA, Article ISSTA045 (<b>ISSTA 2025</b>).<br />
<a href="https://dl.acm.org/doi/10.1145/3728920">[ACM Link]</a>
<a href="papers/2025-ISSTA-Clause2Inv.pdf">[PDF]</a>;
<a href="papers/2025-ISSTA-Clause2Inv-Abstract.md">[Abstract]</a>;
<a href="papers/2025-ISSTA-Clause2Inv-bib.md">[bib]</a>;</p>
</li>
<li><p>Hexu Li, <b>Hengfeng Wei*</b>, Hongrong Ouyang, Yuxing Chen, Na Yang, Ruohao Zhang, Anqun Pan.<br />
<i>Online Timestamp-based Transactional Isolation Checking of Database Systems</i>.<br />
2025 IEEE 41st International Conference on Data Engineering (<b>ICDE</b> 2025).<br />
Hong Kong, 2025, pp. 3738-3750, doi: 10.1109/ICDE65448.2025.00279.<br />
<a href="https://www.computer.org/csdl/proceedings-article/icde/2025/360300d738/26FZC0ImYsU">[IEEE Link]</a>;
<a href="papers/2025-ICDE-TimeKiller.pdf">[PDF]</a>;
<a href="papers/2025-ICDE-TimeKiller-TR.pdf">[Tech Report]</a>;
<a href="papers/2025-ICDE-TimeKiller-Abstract.md">[Abstract]</a>;
<a href="papers/2025-ICDE-TimeKiller-bib.md">[bib]</a>;
<a href="papers/2025-ICDE-TimeKiller-Fund.md">[Funding]</a></p>
</li>
<li><p><b>Hengfeng Wei</b>, Jiang Xiao, Na Yang, Si Liu, Zijing Yin, Yuxing Chen*, Anqun Pan.<br />
<i>Boosting End-to-End Database Isolation Checking via Mini-Transactions</i>.<br />
IEEE 41st International Conference on Data Engineering (<b>ICDE</b> 2025).<br />
Hong Kong, 2025, pp. 3998-4010, doi: 10.1109/ICDE65448.2025.00298.<br />
<a href="https://www.computer.org/csdl/proceedings-article/icde/2025/360300d998/26FZCeQ3uJW">[IEEE Link]</a>;
<a href="papers/2025-ICDE-MiniTesting.pdf">[PDF]</a>;
<a href="papers/2025-ICDE-MiniTesting-TR.pdf">[Tech Report]</a>;
<a href="papers/2025-ICDE-MiniTesting-Abstract.md">[Abstract]</a>;
<a href="papers/2025-ICDE-MiniTesting-bib.md">[bib]</a>;
<a href="papers/2025-ICDE-MiniTesting-Fund.md">[Funding]</a></p>
</li>
<li><p>Xue Jiang, <b>Hengfeng Wei*</b>, Yu Huang, Yuxing Chen, Anqun Pan.<br />
<i>A Generic Specification Framework for Weakly Consistent Replicated Data Types</i>.<br />
in IEEE Transactions on Parallel and Distributed Systems (<b>TPDS</b> 2025),<br />
vol. 36, no. 6, pp. 1338-1353, June 2025, doi: 10.1109/TPDS.2025.3533546.<br />
<a href="https://ieeexplore.ieee.org/document/10852187">[IEEE Link]</a>;
<a href="papers/2025-TPDS-Specs.pdf">[PDF]</a>;
<a href="papers/2025-TPDS-Specs-Abstract.md">[Abstract]</a>;
<a href="papers/2025-TPDS-Specs-bib.md">[bib]</a>;
<a href="papers/2025-TPDS-Specs-Fund.md">[Funding]</a></p>
</li>
</ol>
<h4>2024</h4>
<ol>
<li><p>Guangyuan Wu, Weining Cao, Yuan Yao*, <b>Hengfeng Wei</b>, Taolue Chen, Xiaoxing Ma.<br />
<i>LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference</i>.<br />
In 39th IEEE/ACM International Conference on Automated Software Engineering (<b>ASE</b> 2024),
12 pages.<br />
<a href="https://doi.org/10.1145/3691620.3695014">[ACM Link]</a>;
<a href="papers/2024-ASE-LaM4Inv.pdf">[PDF]</a>;
<a href="papers/2024-ASE-LaM4Inv-Abstract.md">[Abstract]</a>;
<a href="papers/2024-ASE-LaM4Inv-bib.md">[bib]</a></p>
</li>
<li><p>Si Liu, Long Gu, <b>Hengfeng Wei*</b>, David Basin.<br />
<i>Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels</i>.<br />
Proc. ACM Program. Lang. 8, <b>OOPSLA2</b>, Article 302 (October 2024), 29 pages.<br />
<a href="https://doi.org/10.1145/3689742">[ACM Link]</a>
<a href="papers/2024-OOPSLA-Plume.pdf">[PDF]</a>;
<a href="papers/2024-OOPSLA-Plume-Abstract.md">[Abstract]</a>;
<a href="papers/2024-OOPSLA-Plume-bib.md">[bib]</a></p>
</li>
<li><p>Long Gu, Si Liu, Tiancheng Xing, <b>Hengfeng Wei*</b>, Yuxing Chen, David Basin.<br />
<i>IsoVista: Black-box Checking Database Isolation Guarantees</i>.<br />
Proc. VLDB Endow. (<b>VLDB</b> 2024; Demo Track) 17.12 (Aug. 2024), pp. 4325â€“4328.<br />
<a href="https://www.vldb.org/pvldb/vol17/p4325-liu.pdf">[PVLDB Link]</a>
<a href="papers/2024-PVLDB-IsoVista.pdf">[PDF]</a>;
<a href="papers/2024-PVLDB-IsoVista-Abstract.md">[Abstract]</a>;
<a href="papers/2024-PVLDB-IsoVista-bib.md">[bib]</a></p>
</li>
<li><p>Si Liu, Luca Multazzu, <b>Hengfeng Wei</b>, David Basin.<br />
<i>NOC-NOC: Towards Performance-optimal Distributed Transactions</i>.<br />
Proc. ACM Manag. Data, Vol. 2, No. 1 (<b>SIGMOD</b>; June 2024), Article 9. 9:1-9:25.<br />
<a href="https://dl.acm.org/doi/10.1145/3639264">[ACM Link]</a>;
<a href="papers/2024-SIGMOD-NOCNOC.pdf">[PDF]</a>;
<a href="papers/2024-SIGMOD-NOCNOC-Abstract.md">[Abstract]</a>;
<a href="papers/2024-SIGMOD-NOCNOC-bib.md">[bib]</a>;</p>
</li>
</ol>
<h4>2023</h4>
<ol>
<li><p>Kaile Huang, Si Liu, Zhenge Chen, <b>Hengfeng Wei*</b>, David Basin, Haixiang Li, Anqun Pan.<br />
<i>Efficient Black-box Checking of Snapshot Isolation in Databases</i>.<br />
Proc. VLDB Endow. Volume 16, No. 6 (<b>PVLDB</b>; April 2023), 1264â€“1276.<br />
<a href="papers/2023-PVLDB-PolySI.pdf">[PDF]</a>;
<a href="https://arxiv.org/abs/2301.07313">[arXiv Version]</a>;
<a href="papers/2023-PVLDB-PolySI-Abstract.md">[Abstract]</a>;
<a href="papers/2023-PVLDB-PolySI-Fund.md">[Funding]</a>;
<a href="https://dl.acm.org/doi/10.14778/3583140.3583145">[ACM Link]</a>
<a href="papers/2023-PVLDB-PolySI-bib.md">[bib]</a></p>
</li>
</ol>
<h4>2022</h4>
<ol>
<li><p>Xue Jiang, <b>Hengfeng Wei*</b>, Yu Huang.<br />
<i>Tunable Causal Consistency: Specification and Implementation</i>.<br />
The 28th IEEE International Conference on Parallel and Distributed Systems (<b>ICPADS</b>), Jan. 2023.<br /></p>
</li>
<li><p>Yi Huang, <b>Hengfeng Wei</b>.<br />
<i>Incremental Causal Consistency Checking for Read-Write Memory Histories</i>.<br />
The 13th Asia-Pacific Symposium on Internetware (<b>Internetware</b>), June 11-12, 2022.<br /></p>
</li>
<li><p>Hongrong Ouyang, <b>Hengfeng Wei*</b>, Yu Huang, Haixiang Li*, Anqun Pan.<br />
<i>Checking Causal Consistency of MongoDB</i>.<br />
Journal of Computer Science and Technology (<b>JCST</b>), 37(1):128-146, Jan. 2022.<br />
<a href="papers/2022-JCST-MongoDB-CCC.pdf">[PDF]</a> (Journal version of the Internetware&rsquo;2020/2021 paper);
<a href="papers/2022-JCST-MongoDB-CCC-Abstract.md">[Abstract]</a>;
<a href="papers/2022-JCST-MongoDB-CCC-Fund.md">[Funding]</a></p>
</li>
</ol>
<h4>2021</h4>
<ol>
<li><p>Yuqi Zhang, <b>Hengfeng Wei*</b>, Yu Huang*.<br />
<i>Remove-Win: a Design Framework for Conflict-free Replicated Data Types</i>.<br />
The 27th IEEE International Conference on Parallel and Distributed Systems (<b>ICPADS</b>), 2021.<br />
<a href="https://github.com/elem-azar-unis/CRDT-Redis/blob/master/document/rwf-tr.pdf">[PDF (Extended Version)]</a></p>
</li>
<li><p>Manuel Bravo, Alexey Gotsman, Borja de RÃ©gil, <b>Hengfeng Wei</b>.<br />
<i>UniStore: A Fault-tolerant Marriage of Causal and Strong Consistency</i>.<br />
The 2021 USENIX Annual Technical Conference (<b>USENIX ATC</b>), July, 2021.<br />
<a href="papers/2021-ATC-Unistore.pdf">[PDF]</a>;
<a href="papers/2021-ATC-Unistore-arXiv.pdf">[PDF (Extended Version)]</a>;
<a href="papers/2021-ATC-Unistore-Abstract.md">[Abstract]</a>;
<a href="papers/2021-ATC-Unistore-Fund.md">[Funding]</a></p>
</li>
<li><p>Xiaosong Gu, <b>Hengfeng Wei*</b>, Lei Qiao, Yu Huang.<br />
<i>Raft with Out-of-Order Executions (in Chinese)</i>.<br />
Journal of Software (<b>JOS</b>), 32(6):1748-1778, 2021.<br />
<a href="papers/2021-JOS-PRaft.pdf">[PDF]</a>;
<a href="https://www.bilibili.com/video/BV15K411V7KJ?share_source=copy_web">[Video at bilibili]</a>;
<a href="papers/2021-JOS-PRaft-en.pdf">[PDF (in English; ICSI&rsquo;2021) ]</a></p>
</li>
<li><p>Hongrong Ouyang, <b>Hengfeng Wei*</b>, Yu Huang.<br />
<i>Checking Causal Consistency of MongoDB</i>.<br />
The 12th Asia-Pacific Symposium on Internetware (<b>Internetware</b>), May 12-14. 2021.<br />
<a href="papers/2021-Internetware-MongoDB-CCC.pdf">[PDF]</a>;
<a href="https://www.bilibili.com/video/BV1dK4y197FS?share_source=copy_web">[Video at bilibili]</a></p>
</li>
<li><p>Lingzhi Ouyang, Yu Huang, <b>Hengfeng Wei</b>, Jian Lu.<br />
<i>Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores</i>.<br />
IEEE Transactions on Parallel and Distributed Systems (<b>TPDS</b>), 32(4):815-829, Apr. 2021.<br />
<a href="papers/2021-TPDS-ASC.pdf">[PDF]</a>;
<a href="papers/2021-TPDS-ASC-Abstract.md">[Abstract]</a>;
<a href="papers/2021-TPDS-ASC-Fund.md">[Funding]</a>;</p>
</li>
</ol>
<h4>2020</h4>
<ol>
<li><p><b>Hengfeng Wei</b>, Ruize Tang, Yu Huang, Jian Lu.<br />
<i>Jupiter Made Abstract, and Then Refined</i>.<br />
Journal of Computer Science and Technology (<b>JCST</b>), 35(6):1343-1364, Dec. 2020.<br />
<a href="papers/2020-JCST-Jupiter.pdf">[PDF]</a></p>
</li>
<li><p>Xue Jiang, <b>Hengfeng Wei*</b>, Yu Huang.<br />
<i>A Generic Specification Framework for Weakly Consistent Replicated Data Types</i>.<br />
In the Proceeding of the 39th International Symposium on Reliable Distributed Systems (<b>SRDS</b>), Sep. 2020.<br />
<a href="papers/2020-SRDS-SpecFramework.pdf">[PDF]</a></p>
</li>
<li><p>Kaile Huang, Yu Huang, <b>Hengfeng Wei</b>.<br />
<i>Fine-grained Analysis on Fast Implementations of Distributed Multi-writer Atomic Registers</i>.<br />
In the Proceeding of the ACM Symposium on Principles of Distributed Computing (<b>PODC</b>), Aug. 2020.<br />
<a href="papers/2020-PODC-FastAtomic.pdf">[PDF]</a></p>
</li>
<li><p>Xingchen Yi, <b>Hengfeng Wei*</b>, Yu Huang, Lei Qiao, Jian Lu.<br />
<i>TPaxos in PaxosStore: Derivation, Specification and Refinement (in Chinese)</i>.<br />
Journal of Software (<b>JOS</b>), 31(8):2336-2361, 2020.<br />
<a href="papers/2020-JOS-TPaxos.pdf">[PDF]</a>;
<a href="https://www.bilibili.com/video/BV1hV411E7w6?share_source=copy_web">[Video at bilibili]</a></p>
</li>
<li><p>Ye Ji, <b>Hengfeng Wei*</b>, Yu Huang, Jian Lu.<br />
<i>Specifying and Verifying CRDT Protocols Using TLA+ (in Chinese)</i>.<br />
Journal of Software (<b>JOS</b>), 31(5):1332-1352, 2020.<br />
<a href="papers/2020-JOS-CRDT.pdf">[PDF]</a></p>
</li>
</ol>
<h4>2018</h4>
<ol>
<li><p><b>Hengfeng Wei</b>, Yu Huang, and Jian Lu.<br />
<i>Specification and Implementation of Replicated List: the Jupiter Protocol Revisited</i>.<br />
The 22nd International Conference on Principles of Distributed Systems (<b>OPODIS</b>), 2018, 12:1â€“12:16.<br />
<a href="papers/2018-OPODIS-Jupiter.pdf">[PDF]</a></p>
</li>
<li><p><b>Hengfeng Wei</b>, Yu Huang, and Jian Lu.<br />
<i>Brief Announcement: Specification and Implementation of Replicated List: the Jupiter Protocol Revisited</i>.<br />
Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing (<b>PODC</b>), 2018, pp. 81â€“83.<br /></p>
</li>
</ol>
<h4>2017</h4>
<ol>
<li><p><b>Hengfeng Wei</b>, Yu Huang, and Jian Lu.<br />
<i>Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems</i>.<br />
IEEE Trans. Comput. (<b>TC</b>), 66(3), Mar. 2017, pp. 502â€“514.<br />
<a href="papers/2017-TC-PA2AM.pdf">[PDF]</a></p>
</li>
<li><p><b>Hengfeng Wei</b>, Yu Huang, and Jian Lu.<br />
<i>Parameterized and Runtime-Tunable Snapshot Isolation in Distributed Transactional Key-Value Stores</i>.<br />
The IEEE 36th Symposium on Reliable Distributed Systems (<b>SRDS</b>), Sept. 2017, pp. 21â€“33.<br />
<a href="papers/2017-SRDS-RVSI.pdf">[PDF]</a></p>
</li>
</ol>
<h4>2016</h4>
<ol>
<li><p><b>Hengfeng Wei</b>, Marzio De Biasi, Yu Huang, Jiannong Cao, and Jian Lu.<br />
<i>Verifying Pipelined-RAM Consistency over Read</i>Write Traces of Data Replicas/.<br />
IEEE Trans. Parallel Distrib. Syst. (<b>TPDS</b>), 27(5), May 2016, pp. 1511â€“1523.<br />
<a href="papers/2016-TPDS-VPC.pdf">[PDF]</a></p>
</li>
</ol>
<h4>2012</h4>
<ol>
<li><p><b>Hengfeng Wei</b>, Yu Huang, Jiannong Cao, Xiaoxing Ma, and Jian Lu.<br />
<i>Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context</i>.<br />
Proceedings of the 10th IEEE International Conference on Pervasive Computing and Communications (<b>PerCom</b>), 2012, pp. 30â€“38.<br />
<a href="papers/2012-PerCom-CTL3.pdf">[PDF]</a></p>
</li>
</ol>
</div></div>
<div id="footer">
<div id="footer-text">
Page generated 2026-04-08 15:43:37 ÖÐ¹ú±ê×¼Ê±¼ä, by <a href="http://jemdoc.jaboc.net/">jemdoc</a>.
</div>
</div>
</td>
</tr>
</table>
</body>
</html>