https://thufv.github.io/publications/

1<!DOCTYPE html>
2<html>
3
4  <head>
5  <meta charset="utf-8">
6  <meta http-equiv="X-UA-Compatible" content="IE=edge">
7  <meta name="viewport" content="width=device-width, initial-scale=1">
8  <title>THUFV Lab - Publications</title>
9  <meta name="description" content="THUFV Lab -- Publications.">
10  <link rel="stylesheet" href="https://thufv.github.io/css/main.css">
11  <link rel="canonical" href="https://thufv.github.io/publications/">
12<link rel="shortcut icon" type ="image/x-icon" href="https://thufv.github.io/images/favicon.ico">
13
14

15<script>

15
16  (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
17  (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
18  m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
19  })(window,document,'script','https://www.google-analytics.com/analytics.js','ga');
20
21  ga('create', '

21UA-82472331-1

21', 'auto');
22  ga('send', 'pageview');
23

24</script>

24
25
26
27</head>
28
29
30  <body>
31
32    <div class="navbar navbar-default navbar-fixed-top" role="navigation">
33  <div class="container-fluid">
34	<div class="navbar-header">
35	  <button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar-collapse-1" aria-expanded="false">
36		<span class="sr-only">Toggle navigation</span>
37		<span class="icon-bar"></span>
38		<span class="icon-bar"></span>
39		<span class="icon-bar"></span>
40	  </button>
41	
42    <a class="navbar-brand" href="https://thufv.github.io/">Formal Verification Lab @ Tsinghua University</a>
43	</div>
44	<div class="collapse navbar-collapse" id="navbar-collapse-1">
45	  <ul class="nav navbar-nav navbar-right">
46		<li><a href="https://thufv.github.io/">Home</a></li>
47		<li><a href="https://thufv.github.io/team">Team</a></li>
48		<li><a href="https://thufv.github.io/publications">Publications</a></li>
49		<li><a href="https://thufv.github.io/projects">Projects</a></li>
50	  </ul>
51	</div>
52  </div>
53</div>
54
55
56    <div class="container-fluid">
57      <div class="row">
58        <div id="gridid" class="col-sm-12">
59  <h1 id="publications">Publications</h1>
60
61<h2 id="group-highlights">Group highlights</h2>
62
63<p>(For a full list see <a href="#full-list">below</a> or go to <a href="https://scholar.google.com.hk/citations?user=uTnP9v0AAAAJ&amp;hl=zh-CN">Google Scholar</a></p>
64
65<div class="row">
66
67  <div class="col-sm-6 clearfix">
68    <div class="well">
69      <pubtit>Interval Counterexamples for Loop Invariant Learning</pubtit>
70      <p><img src="https://thufv.github.io/images/pubpic/fse2020-artifact.png" class="img-responsive" width="33%" style="float: left" /></p>
71      <p>Interval counterexamples were introduced in this paper, each of which represents a set of counterexamples. With interval counterexamples, the number of iterations for loop invariant learning can be greatly reduced.</p>
72      <p><em>Rongchen Xu, Fei He and Bow-Yaw Wang</em></p>
73      <p><strong>
74<br />
75  <br />
76      <a href="https://doi.org/10.1145/3368089.3409752">ESEC/FSE 2020</a>
77  <br />
78<br />
79  </strong></p>
80      <p class="text-danger"><strong> </strong></p>
81      <p> </p>
82    </div>
83  </div>
84
85  <div class="col-sm-6 clearfix">
86    <div class="well">
87      <pubtit>Control flow-guided SMT solving for program verification</pubtit>
88      <p><img src="https://thufv.github.io/images/pubpic/TBG_ARPES.png" class="img-responsive" width="33%" style="float: left" /></p>
89      <p>This paper is selected as ACM SIGSOFT Distinguished Paper. (TODO) Some more description is needed here.</p>
90      <p><em>Jianhui Chen, Fei He</em></p>
91      <p><strong>
92<br />
93  <br />
94      <a href="https://dl.acm.org/citation.cfm?id=3238218">ASE2018</a>
95  <br />
96<br />
97  </strong></p>
98      <p class="text-danger"><strong> </strong></p>
99      <p> </p>
100    </div>
101  </div>
102
103</div>
104
105<p>   </p>
106
107<h2 id="full-list">Full List</h2>
108
109<p>
110Deadlock Verification via Ordering-Constrained Mutex Modeling <br />
111<em>Pei Wang, Zhilei Han, Zhihang Sun and Fei He </em><br />
112
113CAV 2026 | <a href="https://thufv.github.io/research/cav26">artifact</a>
114
115</p>
116
117<p>
118A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning <br />
119<em>Zhiheng Cai, Zhihang Sun and Fei He </em><br />
120
121FM2026 | <a href="https://doi.org/10.5281/zenodo.19656780">artifact</a>
122
123</p>
124
125<p>
126Accurate Inference of Termination Conditions <br />
127<em>Biting Huang, Zhilei Han and Fei He </em><br />
128
129<a href="https://doi.org/10.1145/3744916.3764568">ICSE 2026</a>
130
131</p>
132
133<p>
134Termination Analysis for Evolving Programs : An Incremental Approach by Reusing Certified Modules <br />
135<em>Fei He, Jitao Han </em><br />
136
137<a href="https://dl.acm.org/doi/abs/10.1145/3428267">OOPSLA 2020</a>
138
139</p>
140
141<p>
142Interval Counterexamples for Loop Invariant Learning <br />
143<em>Rongchen Xu, Fei He and Bow-Yaw Wang </em><br />
144
145<a href="https://doi.org/10.1145/3368089.3409752">ESEC/FSE 2020</a>
146
147</p>
148
149<p>
150Enhancing precision of structured merge by proper tree matching <br />
151<em>Fengmin Zhu, Fei He, Qianshan Yu </em><br />
152
153ICSE 2019
154
155</p>
156
157<p>
158PSpec-SQL: Enabling Fine-Grained Control for Distributed Data Analytics <br />
159<em>Chen Luo, Fei He, Fei Peng, Dong Yan, Dan Zhang and Xin Zhou </em><br />
160
161<a href="https://ieeexplore.ieee.org/document/8703165">IEEE Transactions on Dependable and Secure Computing, 2019, Early Access</a>
162
163</p>
164
165<p>
166Conflict resolution for structured merge via version space algebra <br />
167<em>Fengmin Zhu, Fei He </em><br />
168
169OOPSLA 2018
170
171</p>
172
173<p>
174Control flow-guided SMT solving for program verification <br />
175<em>Jianhui Chen, Fei He </em><br />
176
177<a href="https://dl.acm.org/citation.cfm?id=3238218">ASE2018</a>
178
179</p>
180
181<p>

182SMT-Based Query Tracking for Differentially Private Data Analytics Systems <br />
183<em>Chen Luo, Fei He </em><br />
184
185Frontier of Computer Science, 2018, 12 (6): 1192-1207
186
187</p>
188
189<p>
190Efficient Software Product-Line Model Checking using Induction and a SAT-Solver <br />
191<em>Fei He, Yuan Gao and Liangze Yin </em><br />
192
193Frontier of Computer Science, 2018, 12 (2): 264-279
194
195</p>
196
197<p>
198PSpec: A Formal Specification Language for Fine-Grained Control on Distributed Data Analytics <br />
199<em>Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou and Bow-Yaw Wang </em><br />
200
201ICSE 2017
202
203</p>
204
205<p>
206A True-Concurrency Encoding for BMC of Compositional Systems <br />
207<em>Liangze Yin, Wei Dong, Fei He and Ji Wang </em><br />
208
209The Computer Journal, 2017 July: 1-14
210
211</p>
212
213<p>
214Inferring Software Behavioral Models with MapReduce (extended version) <br />
215<em>Chen Luo, Fei He and Carlo Ghezzi </em><br />
216
217Science of Computer Programming, vol. 145, pp. 13-36, Oct. 2017
218
219</p>
220
221<p>
222Learning-based Assume-Guarantee Regression Verification <br />
223<em>Fei He, Shu Mao and Bow-Yaw Wang </em><br />
224
225CAV 2016
226
227</p>
228
229<p>
230Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes (journal version of the POPL’15 paper) <br />
231<em>Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang and Lijun Zhang </em><br />
232
233TOSEM 2016
234
235</p>
236
237<p>
238Inferring Software Behavioral Models with MapReduce <br />
239<em>Chen Luo, Fei He and Carlo Ghezzi </em><br />
240
241SETTA 2015
242
243</p>
244
245<p>
246VeRV: A Temporal and Data-Concerned Verification Framework for the Vehicle Bus Systems <br />
247<em>Shuo Zhang, Fei He and Ming Gu </em><br />
248
249IEEE INFOCOM 2015
250
251</p>
252
253<p>
254Leveraging Weighted Automata in Composition Reasoning about Concurrent Probabilistic Systems <br />
255<em>Fei He, Xiaowei Gao, Bow-Yaw Wang and Lijun Zhang </em><br />
256
257POPL 2015
258
259</p>
260
261<p>
262Deadlock detection in FPGA design: a practical way <br />
263<em>Dexi Wang, Fei He, Yangdong Deng, Chao Su, Ming Gu, and Jiaguang Sun </em><br />
264
265Tsinghua Science &amp; Technology, 20(2), pp. 212-218, January 2015
266
267</p>
268
269<p>
270Generalized Interface Automata with Multicast Synchronization <br />
271<em>Fei He, Xiaoyu Song, Ming Gu and Jiaguang Sun </em><br />
272
273Frontier of Computer Sciences, 9(1), pp. 1-14, Feb. 2015
274
275</p>
276
277<p>
278Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic <br />
279<em>Min Zhou, Fei He, Xiaoyu Song, Shi He, Gangyi Chen, Ming Gu </em><br />
280
281Theory of Computing Systems, 56(2), pp. 347-371, Feb. 2015
282
283</p>
284
285
286</div>
287
288      </div>
289    </div>
290
291    <div id="footer" class="panel">
292  <div class="panel-footer">
293	<div class="container-fluid">
294	  <div class="row">
295		<div class="col-sm-6">
296			
297		  <p>&copy 2020-2024 THUFV Lab. Powered by <a href="https://jekyllrb.com/">Jekyll</a>.</p>
298		  
299		  <p><a href="https://thufv.github.io/aboutwebsite.html"></a></p>
300		  
301		  <p>We are part of the <a href="http://www.thss.tsinghua.edu.cn/">School of Software</a> at <a href="https://www.tsinghua.edu.cn/en/index.htm">Tsinghua University</a>.</p>
302		</div>
303            
304		<div class="col-sm-6">
305		  Contact:<br />
306		  Room 11-321, East Main Building, Tsinghua University<br />
307		  Beijing 100084, China (<a href="https://goo.gl/maps/QWusT3XwRCNY2Hn19">Maps</a>)<br />
308		</div>
309	  </div>
310	</div>
311  </div>
312</div>
313

314<script src="https://ajax.googleapis.com/ajax/libs/jquery/1.11.3/jquery.min.js"></script>

314

315<script src="https://thufv.github.io/js/bootstrap.min.js"></script>

315
316
317
318  </body>
319
320</html>