-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
656 lines (630 loc) · 33.7 KB
/
index.html
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
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/html">
<head>
<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-2J23RK0R02"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag() {
dataLayer.push(arguments);
}
gtag('js', new Date());
gtag('config', 'G-2J23RK0R02');
</script>
<script async src="//busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<meta name="description" content="homepage">
<link rel="stylesheet" type="text/css" href="
style.css">
<script src="auto.js"></script>
</head>
<body>
<div class="content">
<table align=center cellpadding=35>
<tr>
<td>
<img src="figs/cat.jpeg" width="150" alt="Photo">
</Td>
<Td>
<H2>Yao Peisen</H2>Assistant Professor (ZJU 100 Young Professor) <br>
<a href="https://icsr.zju.edu.cn/">School of Cyber Science and Technology</a>
<br>
<a href="http://www.cs.zju.edu.cn/csen/">College of Computer Science and Technology</a>
<br>
<a href="http://www.cs.zju.edu.cn/csen/">Zhejiang University</a>
<br>
<br> Office: Room 311, Tower B06, ZJU-Hangzhou Global Scientific and Technological Innovation Center <br> Email: [email protected] <br>
<br> Official homepage at ZJU: <a href="https://person.zju.edu.cn/pyao">https://person.zju.edu.cn/pyao</a>
<br>
<br>
</td>
</tr>
</table>
<hr>
<center> [<a href="#publication">
<big>
<b>Publications</b>
</big>
</a>]
[<a href="#awards">
<big>
<b>Awards</b>
</big>
</a>]
[<a href="#software">
<big>
<b>Software</b>
</big>
</a>]
[<a href="#service">
<big>
<b>Service</b>
</big>
</a>]
[<a href="#teaching">
<big>
<b>Teaching</b>
</big>
</a>]
[<a href="#students">
<big>
<b>Students</b>
</big>
</a>]
[<a href="#misc">
<big>
<b>Misc</b>
</big>
</a>]
</center>
<hr noShade size=2.5>
<a name="news"></a>
<h3>News</h3>
<ul>
<li class="item"><img src="figs/new.gif" alt="news">
<a style="color:#FF0000">I am looking for self-motivated students (enrolled in 2025 && 2026)!</a> Please read <a href="html/note-to-prospective-students.html">this</a> if you are a student interested in working with me (e.g., for Ph.D., Master, SRTP, and FYP).
</li>
<li class="item">
<img src="figs/new.gif" alt="news">I am currently on the program committee of <a href="https://2025.splashcon.org/home/sas-2025">SAS 2025</a>, <a href="https://www.sigsac.org/ccs/CCS2025/">CCS 2025</a>, <a href="https://2025.splashcon.org/track/OOPSLA">OOPSLA 2025</a>, <a href="https://conf.researchr.org/home/POPL-2025">POPL 2025</a>, and <a href="https://conf.researchr.org/home/issta-2025">ISSTA 2025</a>. Please consider submitting a paper!
</li>
</ul>
<hr noShade size=2.5>
<h3>Research Interests</h3>I am broadly interested in programming languages, software engineering, and cybersecurity, focusing on techniques that make software secure, usable, and fast.
<h3>Current Research</h3>
<ul>
<li class="item">
Program Analysis and Verification
<ul>
<li class="item">
Path sensitivity
[<a href="https://dl.acm.org/doi/pdf/10.1145/3632743">TOSEM'24</a>]
[<a href="./files/PLDI21Fusion.pdf">PLDI'21a</a>]
[<a href="https://dl.acm.org/doi/10.1145/3395363.3397378">ISSTA'20</a>],
context sensitivity (via CFL-reachability)
[<a href="./files/OOPSLA22-FLARE.pdf">OOPSLA'22a</a>]
</li>
<li class="item">
Alias analysis
[<a href="./files/PLDI24.pdf">PLDI'24</a>]
[<a href="./files/ISSTA24.pdf">ISSTA'24</a> <img src="figs/award.gif" width="18" alt="">]
[<a href="./files/TOSEMAnchor.pdf">TOSEM'23</a>]
[<a href="./files/OOPSLA22-FLARE.pdf">OOPSLA'22a</a>]
</li>
<li class="item">
Numerical analysis
[<a href="">ISSTA'25</a>]
[<a href="./files/ASE23Invariant.pdf">ASE'23a</a>]
[<a href="./files/ICSE22Wit.pdf">ICSE'22</a>]
[<a href="https://dl.acm.org/doi/10.1145/3485495">OOPSLA'21</a>]
[<a href="./files/ASE21TransCode.pdf">ASE'21</a>]
</li>
<li class="item">
Concurrency analysis
[<a href="./files/SECURITY23LockPick.pdf">USENIX Security'23</a>]
[<a href="./files/PLDI21Canary.pdf">PLDI21'b</a>],
change impact analysis
[<a href="./files/ASE23DCLink.pdf">ASE'23b</a>]
</li>
<li class="item">
Fuzzing:
directed
[<a href="./files/SP24Titan.pdf">S&P'24</a>]
[<a href="https://qingkaishi.github.io/public_pdfs/SP22.pdf">S&P'22</a>
<img src="figs/award.gif" width="18" alt="">],
seed sheduling
[<a href="https://5hadowblad3.github.io/files/TDSC.pdf">TDSC'23</a>],
hybrid
[<a href="./files/SP20Pangolin.pdf">S&P'20</a>],
oracle
[<a href="https://dl.acm.org/doi/abs/10.1145/3468264.3468540">ESEC/FSE'21</a>],
configuration
[<a href="https://dl.acm.org/doi/10.1145/3460319.3464803">ISSTA'21</a>]
</li>
</ul>
</li>
<li class="item">
Program Synthesis and Optimizations
<ul>
<li class="item">
Program synthesis for
code search
[<a href="https://arxiv.org/pdf/2305.04316.pdf">ECOOP'23</a>] and
translation [<a href="./files/ASPLOS24.pdf">ASPLOS'24</a>] [<a href="./files/TOSEMKBX.pdf">TOSEM'25</a>]
</li>
<li class="item">
Optimizations of
Java collections [<a href="./files/OOPSLA22Cres.pdf">OOPSLA'22b</a> <img src="figs/award.gif" width="18" alt="">] and
database-backed applications [<a href="./files/ICSE23EqDAC.pdf">ICSE'23</a>]
</li>
</ul>
</li>
<li class="item">
Logic and Automted Reasoning
<ul>
<li class="item">
Symbolic abstraction: application in synthesizing best abstract transformers [<a href="https://dl.acm.org/doi/10.1145/3485495">OOPSLA'21</a>]
</li>
<li class="item">
A formalization of conditional independence [<a href="https://arxiv.org/pdf/2309.05264.pdf">ICSE'24</a>] (for causal discovery)
</li>
</ul>
</li>
</ul>
<a name="publication"></a>
<h3>Selected Publications</h3>
<ul>
<li style="margin-bottom: 10px;">
<a href="">ISSTA 2025: Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions</a>
<br>Guangsheng Fan, Liqian Chen, Banghu Yin, Wenyu Zhang, Peisen Yao, and
Ji Wang
<br>The ACM SIGSOFT International Symposium on Software Testing and Analysis (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="">TOSEM 2025: KBX: Verified Model Synchronization via Formal Bidirectional Transformation</a>
<br>Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, and Kui Ren
<br>ACM Transactions on Software Engineering and Methodology (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/PLDI24.pdf">PLDI 2024: Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis</a>
<br>Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang
<br>The ACM SIGPLAN Conference on Programming Language Design and Implementation (CCF Rank A)
<br><a style="color:#FF0000">The first PLDI paper from ZJU!</a>
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ASPLOS24.pdf">ASPLOS 2024: SIRO: Empowering Version Compatibility in Intermediate Representations via Program Synthesis</a>
<br>Bowen Zhang, Wei Chen, Peisen Yao, Chengpeng Wang, Wensheng Tang, and Charles Zhang
<br>ACM International Conference on Architectural Support for Programming Languages and Operating Systems (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ISSTA24.pdf">ISSTA 2024: Precise Compositional Buffer Overflow Detection via Heap Disjointness</a>
<br>Yiyuan Guo, Peisen Yao, and Charles Zhang<br>
The ACM SIGSOFT International Symposium on Software Testing and Analysis (CCF Rank A)
<br><img src="figs/award.gif" width="20" alt="">
<a style="color:#FF0000">ACM SIGSOFT Distinguished Paper Award</a>
</li>
<li style="margin-bottom: 10px;"><a href="https://dl.acm.org/doi/pdf/10.1145/3632743">TOSEM 2024: Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path Conditions</a>
<br>Wensheng Tang, Dejun Dong, Shijie Li, Chengpeng Wang, Peisen Yao, Jinguo Zhou, and Charles Zhang
<br>ACM Transactions on Software Engineering and Methodology (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="https://arxiv.org/pdf/2309.05264.pdf">ICSE 2024: Enabling Runtime Verification of Causal Discovery Algorithms with Automated Conditional Independence Reasoning</a>
<br> Pingchuan Ma, Zhenlan Ji, Peisen Yao, Shuai Wang, and Kui Ren
<br> The 2024 IEEE/ACM International Conference on Software Engineering (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/SP24Titan.pdf">S&P 2024: Titan: Efficient Multi-target Directed Greybox Fuzzing</a>
<br> Heqing Huang, Peisen Yao, Hung-Chun Chiu, Yiyuan Guo, and Charles Zhang
<br> The 45th IEEE Symposium on Security and Privacy (Oakland) (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ASE23Invariant.pdf">ASE 2023a: Demystifying Template-based Invariant Generation for Bit-Vector Programs</a>
<br> Peisen Yao, Jingyu Ke, Jiahui Sun, Hongfei Fu, Rongxin Wu, and Kui Ren
<br> The 2023 IEEE/ACM Automated Software Engineering Conference (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ASE23DCLink.pdf">ASE 2023b: DCLink: Bridging Data Constraint Changes and Implementations in FinTech Systems</a>
<br>Wensheng Tang, Chengpeng Wang, Peisen Yao, Rongxin Wu, Xianjin Fu, Gang Fan, and Charles Zhang
<br> The 2023 IEEE/ACM Automated Software Engineering Conference (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="https://arxiv.org/pdf/2305.04316.pdf">ECOOP 2023: Synthesizing Conjunctive Queries for Code Search</a>
<br> Chengpeng Wang, Peisen Yao, Wensheng Tang, Gang Fan, and Charles Zhang
<br> European Conference on Object-Oriented Programming (CCF Rank B)
</li>
<li style="margin-bottom: 10px;">
<a href="https://5hadowblad3.github.io/files/TDSC.pdf">TDSC 2023: Balance Seed Scheduling via Monte Carlo Planning</a>
<br> Heqing Huang, Hung-Chun Chiu, Qingkai Shi, Peisen Yao, and Charles Zhang
<br>IEEE Transactions on Dependable and Secure Computing (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ICSE23EqDAC.pdf">ICSE 2023: Verifying Data Constraint Equivalence in FinTech Systems</a>
<br>Chengpeng Wang, Gang Fan, Peisen Yao, Fuxiong Pan, and Charles Zhang
<br>The 2023 IEEE/ACM International Conference on Software Engineering (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/SECURITY23LockPick.pdf">USENIX Security 2023: Place Your Locks Well: Understanding and Detecting Lock Misuse Bugs</a>
<br>Yuandao Cai, Peisen Yao, Chengfeng Ye, and Charles Zhang
<br>The 32nd USENIX Security Symposium (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/TOSEMAnchor.pdf">TOSEM 2023: Anchor: Fast and Precise Value-Flow Analysis for Containers via Memory Orientation</a>
<br> Chengpeng Wang, Wenyang Wang, Peisen Yao, Qingkai Shi, Jinguo Zhou, Xiao Xiao, and Charles Zhang
<br> ACM Transactions on Software Engineering and Methodology (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/OOPSLA22-FLARE.pdf">OOPSLA 2022a: Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis</a>
<br> Qingkai Shi, Yongchao Wang, Peisen Yao, and Charles Zhang
<br> The 37th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/OOPSLA22Cres.pdf">OOPSLA 2022b: Complexity-Guided Container Replacement Synthesis</a>
<br> Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
<br> The 37th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications (CCF Rank A)
<br><img src="figs/award.gif" width="20" alt="">
<a style="color:#FF0000">ACM SIGPLAN Distinguished Paper Award</a>
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ICSE22Wit.pdf">ICSE 2022: Precise Divide-By-Zero Detection with Affirmative Evidence</a>
<br> Yiyuan Guo, Jinguo Zhou, Peisen Yao, Qingkai Shi, and Charles Zhang
<br> The 2022 IEEE/ACM International Conference on Software Engineering (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/SP22Beacon.pdf">S&P 2022: BEACON: Directed Grey-Box Fuzzing with Provable Path Pruning</a>
<br> Heqing Huang, Yiyuan Guo, Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang
<br> The 43rd IEEE Symposium on Security and Privacy (Oakland) (CCF Rank A)
<br>
<img src="figs/award.gif" width="20" alt="">
<a style="color:#FF0000">Google Research Paper Rewards</a>
</li>
<li style="margin-bottom: 10px;">
<a href="">PhD Thesis: Solidifying and Scaling SMT-based Program Analysis, 2022. HKUST</a> <br>
Honorable Mention in the CSE Best Dissertation Award, HKUST
</li>
<li style="margin-bottom: 10px;">
<a href="./files/OOPSLA21SymAbsExtended.pdf">OOPSLA 2021: Program Analysis via Efficient Symbolic Abstraction</a>
<br> Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang <br> The 36th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications (CCF Rank A) <br>
<a style="color:#FF0000">(One of the algorithms has been integrated into SVF)</a>
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ASE21TransCode.pdf">ASE 2021: Transcode: Detecting Status Code Mapping Errors in Large-Scale Systems</a>
<br> Wensheng Tang, Yikun Hu, Gang Fan, Peisen Yao, Rongxin Wu, Guangyuan Bai, Pengcheng Wang, and Charles Zhang<br> The 2021 IEEE/ACM Automated Software Engineering Conference (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/FSE21SparrowTest.pdf">ESEC/FSE 2021: Skeletal Approximation Enumeration for SMT Solver Testing</a>
<br> Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang
<br> The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/ISSTA21FalconFuzz.pdf">ISSTA 2021: Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration</a>
<br> Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang
<br> The 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/PLDI21Fusion.pdf">PLDI 2021a: Path-Sensitive Sparse Analysis without Path Conditions</a>
<br> Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang
<br> The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/PLDI21Canary.pdf">PLDI 2021b: Canary: Practical Static Detection of Inter-Thread Value-Flow Bugs</a>
<br> Yuandao Cai, Peisen Yao, and Charles Zhang
<br> The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="https://dl.acm.org/doi/10.1145/3395363.3397378">ISSTA 2020: Fast Bit-Vector Satisfiability</a>
<br> Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang
<br> The 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (CCF Rank A)
</li>
<li style="margin-bottom: 10px;">
<a href="./files/SP20Pangolin.pdf">S&P 2020: Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction</a>
<br> Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang
<br> The 41st IEEE Symposium on Security and Privacy (Oakland) (CCF Rank A)
</li>
</ul>
<!--
<p id="footnote-1">* means corresponding author.</p> -->
<hr noShade size=2.5>
<a name="awards"></a>
<h3>
<strong>Honors & Awards</strong>
</h3>
<ul>
<li class="item">ACM SIGSOFT Distinguished Paper Award (ISSTA 2024)
</li>
<li class="item">CCF-Huawei Innovation Research Award (2023-formal method, 2024-compilers)
</li>
<li class="item">NSFC Excellent Young Scientists Program (Overseas) 国家高层次青年人才计划
</li>
<li class="item">Google Research Paper Rewards, 2022
</li>
<li class="item">ACM SIGPLAN Distinguished Paper Award (OOPSLA 2022)
</li>
<li class="item">Qizhen Scholar of ZJU (浙江大学启真优秀青年学者)
</li>
<li class="item">Honorable Mention in the CSE Best Dissertation Award, HKUST, 2022
</li>
<li class="item">Huawei Distinguished Collaborator, 2021
</li>
<li class="item">Outstanding Undergraduate Award, HUST
</li>
<li class="item">Second Place in Linpack Track (We broke the world record!), ASC 2014
</li>
<li class="item">Technical Excellence Award, Unique Hackday
</li>
</ul>
<hr noShade size=2.5>
<a name="software"></a>
<h3>Software</h3>
<ul>
<li class="item">Current Projects
<ul>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://github.com/ZJU-Automated-Reasoning-Group/canary">canary</a> is a static analyzer for C/C++ source code and binaries built on top of LLVM, CUDD, capstone, Z3, and Crab</a> (<a href="">ISSTA'25</a>)
</p>
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="">???</a> is a compiler optimization tool based on LLVM, Z3, and LLM
</p>
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://github.com/ZJU-Automated-Reasoning-Group/efmc">efmc</a> is an SMT-based software model checker (<a href="./files/ASE23Invariant.pdf">ASE'23a</a>)
</p>
</li>
<li class="item">
<a href="https://github.com/ZJU-Automated-Reasoning-Group/arlib">arlib</a> is a library for playing with various automated reasoning tasks, such as model counting, quantifier elimination, etc (<a href="">ICSE'24</a>)
<ul>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://github.com/ZJU-Automated-Reasoning-Group/pyomt">pyomt</a>: a solver for Optimization Modulo Theory (OMT) problems over bit-vectors, integers, and reals
</p>
</li>
<li class="item">
<a href="">z3-owl</a>: a data-driven parallel constraint solving engine
</li>
</ul>
</li>
</ul>
</li>
<br>
<li>Former Projects
<ul>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://www.sourcebrella.com/">Pinpoint</a> is an SMT-based, industrial-strength static analysis framework (<a href="https://dl.acm.org/doi/10.1145/3453483.3454099">PLDI'21a</a>, <a href="https://dl.acm.org/doi/10.1145/3453483.3454099">PLDI'21b</a>, <a href="./files/ASE21TransCode.pdf">ASE'21</a>, <a href="./files/ICSE22Wit.pdf">ICSE'22</a>, <a href="./files/OOPSLA22-FLARE.pdf">OOPSLA'22a</a>, <a href="./files/SECURITY23LockPick.pdf">USENIX Security'23</a>, <a href="./files/TOSEMAnchor.pdf">TOSEM'23</a>, <a href="">PLDI'24</a>...) <br>
<ul>
<li class="item">Pinpoint has found <a href="https://fusion-scan.github.io/">hundreds of bugs</a> in many mature and fundamental open-source projects, including Linux Kernel, FreeBSD, Firefox, HBase, OpenSSL, PostgreSQL, MySQL, Memcached, Redis, FFmpeg, Apache HTTPd, Git, Python, Tmux, Vim, and many others
</li>
<li>Pinpoint was commercialized at <a href="https://www.sourcebrella.com/">Sourcebrella Inc</a>, which was acquired by Ant Group in 2020
</li>
</ul>
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="">Pangolin</a> is a fuzzer for C/C++ source code and binaries (Pangolin <a href="files/HybridFuzz-Preprint.pdf">S&P'20</a>, Beacon <a href="files/HybridFuzz-Preprint.pdf">S&P'22</a>, BeliefFuzz <a href="">TDSC'23</a>, Titan <a href="./files/SP24Titan.pdf">S&P'24</a>)
<ul>
<li class="item">A partial of of detected vulnerabilities in open-source projects can be found <a href="https://outstanding-hydrogen-2d1.notion.site/Trophies-aef45e1245a64528bd8ec111b475e03b">here</a>
</li>
<li class="item">Our work has been successfully deployed in the Huawei tool-chain and detected more than 1000+ bugs! We have thus received the Huawei Distinguished Collaborator 2021 award
</li>
</ul>
</p>
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://github.com/EqDAC/EqDACTool">EqDAC</a> is an equivalence checker for verifying data constraint equivalence </a>(<a href="./files/ICSE23EqDAC.pdf">ICSE'23</a>)
</p>
<ul>
<li class="item">EqDAC has been deployed in Ant Group, a global FinTech company with 1 billion active users
</li>
</ul>
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="">Cres</a> is a program synthesizer for code optimization [<a href="./files/OOPSLA22Cres.pdf">OOPSLA'22b</a>
<img src="figs/award.gif" width="18" alt="">] and code search [<a href="https://arxiv.org/pdf/2305.04316.pdf">ECOOP'23</a>]
</li>
<li class="item">
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<a href="https://github.com/ZJU-Automated-Reasoning-Group/smtfuzz">smtfuzz</a> is a fuzzer for SMT solvers (<a href="https://dl.acm.org/doi/abs/10.1145/3468264.3468540">ESEC/FSE'21</a>, <a href="https://dl.acm.org/doi/10.1145/3460319.3464803">ISSTA'21</a>)
<ul>
<li class="item">Smtfuzz has found <a href="https://smtfuzz.github.io/">hundreds of bugs</a> in several state-of-the-art SMT solvers and first-order theorem provers, such as Z3, CVC5, Yices2, STP, Boolector, MathSAT5, SMTInterpol, OpenSMT, SMT-RAT, DReal, SPASS, and Vampire
</li>
<li class="item">You may try a simplified implementation of the random formula generator by "pip install smtfuzz"
</li>
</ul>
</p>
</li>
</ul>
</ul>
<hr noShade size=2.5>
<a name="service"></a>
<h3>Service</h3>
<ul>
<li>
Chair or Co-chair: CCF ChinaSoft'23优秀博士生论坛
</li>
<li>
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
Technical Program Committee:
<ul>
<li class="item">
<b>POPL</b>: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2025) (first PC from ZJU)
<li class="item"><b>PLDI</b>: ACM SIGPLAN Conference on Programming Language Design and Implementation (2023) (first PC from ZJU)</li>
<li class="item"><b>OOPSLA</b>: ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Application (2025) (first PC from ZJU)</li>
<li class="item"><b>ISSTA</b>: ACM SIGSOFT International Symposium on Software Testing and Analysis (2025, 2024)</li>
<li class="item"><b>SAS</b>: Static Analysis Symposium (2025)</li>
<li class="item"><b>CCS</b>: ACM Conference on Computer and Communications Security (2025, 2024)</li>
<li class="item"><b>EuroS&P</b>: IEEE European Symposium on Security and Privacy (2024)</li>
<li class="item"><b>RAID</b>: International Symposium on Research in Attacks, Intrusions and Defenses (2023)</li>
<li class="item"><b>SETTA</b>: Symposium on Dependable Software Engineering. Theories, Tools and Applications (2024) </li>
<li class="item"><b>ChinaSoft</b> (2024, 2023)</li>
</ul>
</p>
</li>
<li style="margin-bottom: 10px;">
Journal Reviewer:
<p style="text-align:justify; text-justify:inter-ideograph; margin-right: 5mm">
<ul>
<li class="item"><b>TOPLAS</b>: ACM Transactions on Programming Languages and Systems</li>
<li class="item"><b>TOSEM</b>: ACM Transactions on Software Engineering and Methodology</li>
<li class="item"><b>TOPS</b>: ACM Transactions on Privacy and Security</li>
<li class="item"><b>TKDD</b>: ACM Transactions on Knowledge Discovery from Data</li>
<li class="item"><b>TR</b>: IEEE Transactions on Reliability</li>
<li class="item">电子学报，软件学报，计算机学报</li>
</ul>
</p>
</li>
<li class="item">
Artifact Evaluation Committee: PLDI (2024, 2023), OOPSLA (2024), ICSE 2024), USENIX Security (2023), ATC (2022), OSDI (2022)<br>
</li>
<li class="item">
Program Committee of other Tracks: EuroSys'25 (Shadow PC), ASE'24 (Industry), SNAER'24 (Demo), OOPSLA'23 (SRC)
</li>
<li class="item">
Conference Reviewer/Sub-reviewer/Co-reviewer: ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17
</li>
</ul>
<a name="mentoring"></a>
<h3>Mentoring</h3>
<ul>
<li class="item">
Long-term mentor of <a href="https://www.sigplan.org/LongTermMentoring/">SIGPLAN-M
</a>
</li>
</ul>
<hr noShade size=2.5>
<a name="teaching"></a>
<h3>Teaching</h3>
<ul>
<!--
<li class="item">
<a href="teaching/security24.html">Software Security (Fall 2024, Software Analysis Part), UG Course, ZJU</a>
</li>
-->
<li class="item">
<a href="teaching/compilers25.html">Principles of Compilers (Spring 2025), UG Course, ZJU</a>
</li>
<li class="item">
<a href="">Principles of Compilers (Spring 2024), UG Course, ZJU</a>
</li>
<li class="item">
信息安全前沿技术和研究方法论, 研究生课程 (2023 春夏, 2024 春夏), 形式化方法部分, ZJU
</li>
<li class="item">
COMP4632: Practicing CyberSecurity: Attacks and Counter-measures, Teaching Assistant, HKUST
</li>
<li class="item">
COMP3021: Java Programming, Teaching Assistant, HKUST
</li>
<li class="item">
COMP3511: Operating System, Teaching Assistant, HKUST
</li>
</ul>
<hr noShade size=2.5>
<a name="students"></a>
<h3>Students</h3>
<ul>
<li class="item">
Current Students:
<ul>
<li class="item">Postgraduate Students: Weiqi Wang (Master from 23), Yuan Li (Ph.D. from 23), Hanrui Zuo (Ph.D. from 24), Zinan Gu (Master from 24), Guowei Tian (Master from 24), Hanyun Jiang (Master from 25), ??? (Ph.D. from 25)
</li>
<li class="item">Co-supervised Students ("导师组"成员): Jianhong Zhao
</li>
<li class="item">Final Year Project: Chenhao Gao, Yaoyang Ye, Jiening Siow
</li>
</ul>
</li>
<li class="item">
Former Mentees
<ul>
<li class="item">Intern (>=3 months): Ruiyu Zhou (UG@CUHK(SZ), 23), Chenya Sun (UG@BUAA, 24)
</li>
<li class="item">Final Year Project: Ruqing Yang, Xutao Zhou, Yitong Li, Xinyue Cai, Haobai Yin, Haowei Cao, Yichi Zhang, Mingming Luo
</li>
</ul>
</li>
</ul>
<hr noShade size=2.5>
<a name="misc"></a>
<h3>Misc</h3>
<ul>
<li class="item">
<a href="http://www.cs.wisc.edu/wpis/talks/WritingResearchPapers.pptx">Tips on writing a research paper</a> by Thomas Reps [<a href="https://www.pldi21.org/prerecorded_plmw.2.html">video</a>]
</li>
<li class="item">
<a href="https://homes.cs.washington.edu/~mernst/advice/write-technical-paper.html">Writing a technical paper</a> by Michael Ernst
</li>
<li class="item">
<a href="http://www.tcse.cn/~wsdou/advice/research%20tips-su.pdf">Doing research in software analysis: lessons and tips</a> by Zhendong Su
</li>
<li class="item">
<a href="html/reading.html">Some interesting papers</a>
</li>
<li class="item">
<a>Automated reasoning for logic and programs (ing...)</a>
</li>
<li class="item">
<a>Lecture notes on principles of compliers (ing...)</a>
</li>
</ul>
</div>
<a name="talks"></a>
<h3>
<strong>Invited Talks</strong>
</h3>
<ul>
<li class="item">
Optimization Modulo Theory (OMT) Solving for Program Analysis, ISCAS, 2024.11
</li>
<li class="item">
A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis, CCF ChinaSoft'24 顶会顶刊论坛, 2024.11
</li>
<li class="item">
Program Analysis via Symbolic Abstraction, Shanghai Jiao Tong University, 2024.06
</li>
<li class="item">
Program Analysis via Symbolic Abstraction, Nanjing University, 2023.12
</li>
<li class="item">
Program Analysis via Symbolic Abstraction, CCF Young Computer Scientists & Engineers Forum, 2023.11
</li>
<li class="item">
Program Analysis via Symbolic Abstraction, HCP'23 (第六届难解问题的表示、算法与应用研讨会), 2023.07
</li>
<li class="item">
高精度静态数值缺陷分析 [<a href="files/chinasoft22.pdf">slide</a>], CCF ChinaSoft'22 高可信嵌入式软件工程技术论坛，2022.11
</li>
<li class="item">
Complexity-Guided Container Replacement Synthesis, CCF ChinaSoft'22 顶会顶刊论坛, 2022.11
</li>
<li class="item">
Program Analysis via Symbolic Abstraction [<a href="files/symbolic_abstraction_intro.pdf">slide</a>], SIG-Program Analysis, 2022.10
</li>
<li class="item">
Introduction to Metamorphic Testing [<a href="files/metamorphic_testing_intro.pdf">slide</a>], System Security Summer School, Zhejiang University
</li>
<li class="item">
Solidifying and Scaling SMT-based Program Analysis, Xiamen University
</li>
<li class="item">
Solidifying and Scaling SMT-based Program Analysis, Nanjing University
</li>
<li class="item">
Scaling and Solidifying SMT-based Program Analysis, Shanghai Jiao Tong University
</li>
<li class="item">
Scaling and Solidifying SMT-based Program Analysis, ShanghaiTech University
</li>
</ul>
<hr noShade size=2.5>
<a name="xxx"></a> Visitors: <span id="busuanzi_value_site_pv"></span>
</body>
</html>
<!--
<li class="item">
<a href=" https://openpal.github.io/TypeAndProof/">Type and proof (unfinished tutorial)</a>
</li>
-->