-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpublication.html
414 lines (315 loc) · 27.9 KB
/
publication.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
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
<link rel="icon" type="image/png" href="images/icon.png">
<link href="css/metro-bootstrap.css" rel="stylesheet">
<!--<link href="css/metro-bootstrap-responsive.css" rel="stylesheet">-->
<link href="css/iconFont.css" rel="stylesheet">
<!-- Load JavaScript Libraries -->
<script src="js/jquery/jquery.min.js"></script>
<script src="js/jquery/jquery.widget.min.js"></script>
<!-- Metro UI CSS JavaScript plugins -->
<script src="js/load-metro.js"></script>
<!-- Local JavaScript -->
<script src="js/docs.js"></script>
<script src="js/github.info.js"></script>
<title>Yongwang ZHAO's Homepage</title>
<style type="text/css">
.container {
width: 1040px;
}
.paperlable {
background: #dddddd;
border-radius: 7px;
padding-left: 5px;
padding-right: 5px;
padding-top: 0px;
padding-bottom:2px;
align: center;
}
</style>
</head>
<body class="metro" style="text-align:justify;">
<div class="container">
<div class="margin10 nrm nlm" data-load="header.html"></div>
<div class="main-content clearfix">
<div class="tab-control" data-role="tab-control" style="float:left;width:100%;">
<ul class="tabs">
<li class="active"><a href="#_page_1">Home <i class="icon-arrow-right-5"></i> Papers </a></li>
</ul>
<div class="panel" id="journal" data-role="panel" style="width:100%;">
<div class="panel-header" style="background:#dddddd;font-size:14pt;"><span class="fg-darker"><b>主要论著 Selected Publication (# Corresponding Author) [所有论文见<a href="http://dblp.uni-trier.de/pers/hd/z/Zhao:Yongwang" target="_blank"> DBLP Records </a>]</b></span></div>
<div class="panel-content margin10 fg-dark nlp nrp" style="width:98%;font-size:13pt;margin-top:-5pt;margin-bottom:-5pt">
<ol>
<li>
<text class="paperlable">[OOPSLA 2025]</text>
Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, <strong>Yongwang Zhao</strong>, "A complete formal semantics of eBPF instruction set architecture for Solana", <em>
<u>ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2025) </u></em>, accepted (<em><strong>CCF A</strong></em>)
<a href="https://trust2proj.github.io/doc/OOPSLA25.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[TOPLAS 2021]</text>
David Sanan, <strong>Yongwang Zhao#</strong>, Yang Liu, Shangwei Lin, "CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee", <em>
<u>ACM Transactions on Programming Languages and Systems (TOPLAS) </u></em>, Vol. 43, No. 1, February 2021, pp. 2:1 - 2:46 (<em><strong>CCF A</strong></em>)
<a href="https://dl.acm.org/doi/pdf/10.1145/3436808" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[TOSEM 2025]</text>
Jianhong Zhao, <strong>Yongwang Zhao#</strong>, Peisen Yao, Fanlang Zeng, Bohua Zhan, and Kui Ren, "KBX: Verified Model Synchronization via Formal Bidirectional Transformation", <em>
<u>ACM Transactions on Software Engineering and Methodology (TOSEM)</u></em>, Volume 34, Issue 2, Article No. 43, January 25, 2025, Pages 1 - 40 (<em><strong>CCF A</strong></em>)
</li>
<li>
<text class="paperlable">[TDSC 2024]</text>
Jilin Hu, Fanlang Zeng, <strong>Yongwang Zhao#</strong>, Zhuoruo Zhang, Leping Zhang, Jianhong Zhao, Rui Chang, and Kui Ren, "ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile", <em>
<u>IEEE Transactions on Dependable and Secure Computing (TDSC)</u></em>, Volume 21, Issue 6, November/December 2024, pp. 5341 - 5358 (<em><strong>CCF A</strong></em>)
</li>
<li>
<text class="paperlable">[TDSC 2023]</text>
Xinliang Miao, Rui Chang, Jianhong Zhao, <strong>Yongwang Zhao</strong>, Shuang Cao, Yulong Zhang, Tao Wei, Liehui Jiang, and Kui Ren, "CVTEE: A Compatible Verified TEE Architecture with Enhanced Security", <em>
<u>IEEE Transactions on Dependable and Secure Computing (TDSC)</u></em>, Volume 20, Issue 1, 01 Jan.-Feb. 2023, pp. 377 - 391 (<em><strong>CCF A</strong></em>)
</li>
<li>
<text class="paperlable">[FM 2021]</text> Wenjing Xu, <strong>Yongwang Zhao#</strong>, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang and Shihong Zou, "Apply Formal Methods in Certifying the SyberX High-Assurance Kernel", <em>
<u> In Proceedings of 24th International Symposium on Formal Methods (FM 2021) </u></em>, 20-26 November, 2021, Beijing, China, pp. 788 - 798.
<a href="https://link.springer.com/content/pdf/10.1007/978-3-030-90870-6_46.pdf" target="_blank"><strong>[PDF download]</strong></a> (<em><strong>CCF A</strong></em>)
</li>
<li>
<text class="paperlable">[FM 2019]</text>
<strong>Yongwang Zhao</strong>, David Sanan, Fuyuan Zhang, Yang Liu, "A Parametric Rely-guarantee Reasoning Framework for Concurrent Reactive Systems", <em>
<u>23rd International Symposium on Formal Methods (FM 2019)</u></em>, Oct 7-11, 2019, Porto, Portugal, pp. 161-178 (<em><strong>CCF A</strong></em>)<a href="https://link.springer.com/content/pdf/10.1007/978-3-030-30942-8_11.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[CAV 2019]</text>
<strong>Yongwang Zhao</strong>, David Sanan, "Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS", <em>
<u>31st International Conference on Computer-Aided Verification (CAV 2019)</u></em>, July 15-18, 2019, New York City, NY, USA, pp. 515-533 (<em><strong>CCF A</strong></em>)<a href="https://link.springer.com/content/pdf/10.1007/978-3-030-25543-5_29.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[TDSC 2019]</text>
<strong>Yongwang Zhao</strong>, David Sanan, Fuyuan Zhang, Yang Liu, "Refinement-based Specification and Security Analysis of Separation Kernels", <em>
<u>IEEE Transactions on Dependable and Secure Computing (TDSC)</u></em>, Volume 16, Issue 1, January 2019, pp. 127 - 141 (<em><strong>CCF A</strong></em>)
<a href="https://ieeexplore.ieee.org/document/7862167" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[FM 2018]</text>
Fuyuan Zhang, <strong>Yongwang Zhao</strong>, David Sanan, Yang Liu, Alwen Tiu, Shang-wei Lin, Jun Sun, "Compositional Reasoning for Shared-variable Concurrent Programs",
<em><u>22nd International Symposium on Formal Methods (FM 2018)</u></em>, 15-17 July 2018, Oxford UK, pp. 523-541 (<em><strong>CCF A</strong></em>)
<a href="https://link.springer.com/content/pdf/10.1007/978-3-319-95582-7_31.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[SCIS 2024]</text>
古金宇, 李浩, 夏虞斌, 管海兵,丁佐华, <strong>赵永望</strong>, 陈海波. BrickOS: 面向异构硬件资源的积木式内核. 中国科学: 信息科学, 2024, 54: 491–513. (<em><strong>CCF A</strong></em>) <a href="http://scis.scichina.com/cn/2024/SSI-2022-0413.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[TACAS 2024]</text>
Leping Zhang, <strong>Yongwang Zhao#</strong>, Jianxin Li, "A Comprehensive Specification and Verification of the L4 Microkernel API", <em><u>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024, ETAPS)</u></em>, Luxembourg City, Luxembourg, 6–11 April 2024, pp. 217 - 234 (<em><strong>CCF B, Top conf. in formal methods</strong></em>) <a href="https://link.springer.com/chapter/10.1007/978-3-031-57249-4_11" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[STVR 2025]</text>
Feng Zhang, <strong>Yongwang Zhao#</strong>, Yang Liu, Jun Sun, "A Comprehensive Formal Specification of ARINC 653 with Conformity Proof", <em><u>Software Testing, Verification and Reliability (STVR)</u></em>, Volume 35, Issue 1, January 2025, pp. 1 - 17 (<em><strong>CCF B</strong></em>) <a href="https://doi.org/10.1002/stvr.1901" target="_blank"><strong>[Link]</strong></a>
</li>
<li>
<text class="paperlable">[FCS 2024]</text>
Jinhui Kang, Jianhong Zhao, <strong>Yongwang Zhao#</strong>, "K-SELinux: Formal Analysis and Verification of SELinux Policies via Semantic Execution", <em><u>Frontiers of Computer Science</u></em>, 2024, pp. XXX - YYY (Accepted) (<em><strong>CCF B</strong></em>)
</li>
<li>
<text class="paperlable">[FCS 2017]</text>
<strong>Yongwang Zhao</strong>, Zhibin Yang, Dianfu Ma, "A survey on formal specification and verification of separation kernels", <em><u>Frontiers of Computer Science</u></em> , Volume 11, Issue 4, August 2017, pp. 585 – 607. <a href="https://journal.hep.com.cn/fcs/EN/article/downloadArticleFile.do?attachType=PDF&id=17603" target="_blank"><strong>[PDF download]</strong></a> (<em><strong>CCF B</strong></em>)
</li>
<li>
<text class="paperlable">[TACAS 2016]</text>
<strong>Yongwang Zhao</strong>, David Sann, Fuyuan Zhang, Yang Liu, "Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication", <em>22nd <u>International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016, ETAPS)</u></em>, 2-8 April 2016, Eindhoven, The Netherlands, pp. 791-810 (<em><strong>CCF B, Top conf. in formal methods</strong></em>) <a href="papers/TACAS2016.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[FAC 2023]</text>
Feng Zhang, Leping Zhang, <strong>Yongwang Zhao#</strong>, Yang Liu, Jun Sun, "Refinement-Based Specification and Analysis of Multi-Core ARINC 653 Using Event-B", <em><u>Formal Aspects of Computing</u></em>, Volume 35, Issue 4, November, 2023, Article No.24, pp 1–29. (<em><strong>CCF B</strong></em>) <a href="https://dl.acm.org/doi/10.1145/3617183" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[FCS 2021]</text>
Shahbaz Ali, Hailong Sun, <strong>Yongwang Zhao#</strong>, "Model Learning: A Survey on Foundation, Tools and Applications", <em><u>Frontiers of Computer Science</u></em>, Volume 15, Issue 5, October 2021, pp. 1 - 22.
<a href="https://journal.hep.com.cn/fcs/EN/article/downloadArticleFile.do?attachType=PDF&id=25927" target="_blank"><strong>[PDF download]</strong></a> (<em><strong>CCF B</strong></em>)
</li>
<li>
<text class="paperlable">[TACAS 2017]</text>
David Sanan, <strong>Yongwang Zhao</strong>, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu, "CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs",
<em><u>23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, ETAPS)</u></em>, 22-29 April 2017, Uppsala, Sweden, pp. 481-498 (<em><strong>CCF B, Top conf. in formal methods</strong></em>) <a href="https://link.springer.com/content/pdf/10.1007/978-3-662-54577-5_28.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[ISSRE 2015]</text>
<strong>Yongwang Zhao</strong>, Zhibin Yang, David Sanan, Yang Liu, "Event-based Formalization of Safety-critical Operating System Standards", <em><u>26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015)</u></em>, November 2–5, 2015, Washington DC, USA, pp. 281-292 (<em><strong>CCF B</strong></em>) <a href="papers/ISSRE2015.pdf" target="_blank"><strong>[PDF download]</strong></a>.
</li>
<li>
<text class="paperlable">[ISSRE 2023]</text>
Fanlang Zeng, Zhuoruo Zhang, Rui Chang, Chenyang Yu, Zijun Zhang, <strong>Yongwang Zhao</strong>, "Lark: Verified Cross-Domain Access Control for Trusted Execution Environments", <em><u>34th IEEE International Symposium on Software Reliability Engineering (ISSRE 2023)</u></em>, Florence, Italy, October 9 - 12, 2023, pp. 160 - 171 (<em><strong>CCF B</strong></em>) <a href="https://ieeexplore.ieee.org/document/10301232/" target="_blank"><strong>[PDF download]</strong></a>.
</li>
<li>
<text class="paperlable">[ICWS 2023]</text>
Zhuoruo Zhang, Jilin Hu, Chenyang Yu, Rui Chang, <strong>Yongwang Zhao</strong>, "VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks", <em>
<u>International Conference on Web Services (ICWS 2023) </u></em>, JULY 2-8, 2023, CHICAGO, ILLINOIS USA, pp. 71 - 77.
(<em><strong>CCF B</strong></em>) <a href="https://ieeexplore.ieee.org/document/10248266/" target="_blank"><strong>[PDF download]</strong></a>.
</li>
<li>
<text class="paperlable">[SETTA 2024]</text>
Jiayi Lu, Shenghao Yuan, David Sanan, <strong>Yongwang Zhao</strong>, "Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness", <em>
<u>10th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2024) </u></em>, Hong Kong, China, November 26–28, 2024, pp. 197-216.
(<em><strong>CCF C</strong></em>) <a href="https://link.springer.com/chapter/10.1007/978-981-96-0602-3_11" target="_blank"><strong>[PDF download]</strong></a>.
</li>
<li>
<text class="paperlable">[Internetware 2023]</text>
Hao Xu, <strong>Yongwang Zhao#</strong>, "Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving", <em>
<u>14th Asia-Pacific Symposium on Internetware (Internetware 2023) </u></em>, August 4 - 6, 2023, Hangzhou, China, pp. 313–322.
(<em><strong>CCF C</strong></em>) <a href="https://dl.acm.org/doi/10.1145/3609437.3609460" target="_blank"><strong>[PDF download]</strong></a>.
</li>
<li>
<text class="paperlable">[Internetware 2022]</text>
Xinliang Miao, Fanlang Zeng, Rui Chang, Chenyang Yu, Zijun Zhang, Liehui Jiang, <strong>Yongwang Zhao</strong>, "Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE", <em>
<u>13th Asia-Pacific Symposium on Internetware (Internetware 2022) </u></em>, June 11-12, 2022, Hohhot, China, pp. 252–261. (<em><strong>CCF C</strong></em>)
<a href="https://dl.acm.org/doi/10.1145/3545258.3545281" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[ICFEM 2022]</text>
Ke Jiang, Tianwei Zhang, David Sanan, <strong>Yongwang Zhao</strong>, Yang Liu, "A Novel Formal Methodology for Verification of Side-channel Vulnerabilities in Cache Architectures", <em>
<u>23rd International Conference on Formal Engineering Methods (ICFEM 2022) </u></em>, October 24-27, 2022, Madrid, Spain, pp. 190–208. (<em><strong>CCF C</strong></em>)
<a href="https://link.springer.com/chapter/10.1007/978-3-031-17244-1_12" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
蔡少伟, 陈振邦, 王戟, 詹博华, <strong>赵永望</strong>. "约束求解与定理证明专题前言".软件学报, 2023, 34(8):3465-3466.
<a href="https://www.jos.org.cn/jos/article/issue/2023_34_8" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
章乐平, <strong>赵永望#</strong>, 王布阳, 李悦欣, 冯潇潇. "L4 虚拟内存子系统的形式化验证". 软件学报, 2023年, 第34卷, 第8期.
<a href="http://www.jos.org.cn/jos/article/abstract/6869" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
曾凡浪, 常瑞, 许浩, 潘少平, <strong>赵永望</strong>. "基于精化的TrustZone多安全分区建模与形式化验证". 软件学报, 2023年, 第34卷, 第8期.
<a href="http://www.jos.org.cn/jos/article/abstract/6866" target="_blank"><strong>[PDF download]</strong></a>
</li>
<!--
<li>
潘少平, 常瑞, 张子君, <strong>赵永望</strong>. "可信执行环境的运行时安全形式化验证技术". Chinasoft 2022 (软件学报 形式化方法与应用专刊).
</li>-->
<li>
曹钦翔, 詹博华, <strong>赵永望</strong>. "定理证明理论与应用专题前言".软件学报, 2022, 33(6):2113-2114.
<a href="http://jos.org.cn/jos/article/issue/2022_33_6" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
苗新亮, 常 瑞, 潘少平, <strong>赵永望</strong>, 蒋烈辉. "可信执行环境访问控制建模与安全性分析".软件学报, 2022.
<a href="http://www.jos.org.cn/jos/article/abstract/6612" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<text class="paperlable">[SETTA 2020]</text>
<strong>Yongwang Zhao</strong>, "Rely-Guarantee Reasoning About Concurrent Reactive Systems: Framework, Languages Integration and Applications (Invited Talk)", <em>
<u>6th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2020)</u></em>, November 24–27, 2020, Guangzhou, China.
<a href="https://link.springer.com/content/pdf/bfm%3A978-3-030-62822-2%2F1.pdf" target="_blank"><strong>[PDF download]</strong></a> (<em><strong>CCF C</strong></em>)
</li>
<li>
<text class="paperlable">[TASE 2020]</text>
Wenjing Xu, <strong>Yongwang Zhao#</strong>, Dianfu Ma, Yuxin Zhang, "Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles", <em>
<u>14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020)</u></em>, December 11-13, 2020, Hangzhou, China, pp. xxx-yyy (<em><strong>CCF C</strong></em>)
<a href="https://ieeexplore.ieee.org/document/9405321" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
<strong>赵永望</strong>,刘杨,王戟. "系统软件构造与验证技术专题前言".软件学报, 2020, 31(5):1241-1242.
<a href="http://www.jos.org.cn/jos/article/issue/2020_31_5" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
李鼎基, 糜泽羽, 吴保东, 陈逊, <strong>赵永望</strong>, 丁佐华, 陈海波, "利用跨虚拟机零下陷通信的加速器虚拟化框架", 软件学报,2020,31(10):3019-3037
</li>
<!--
<li>
<strong>Yongwang Zhao</strong>, David Sanan, Fuyuan Zhang, Yang Liu, "An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems", arXiv:1810.07855 (2018) <a href="https://arxiv.org/pdf/1810.07855.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
-->
<li>
<text class="paperlable">[ISORC 2019]</text>
Feng Zhang, <strong>Yongwang Zhao#</strong>, Dianfu Ma, Wensheng Niu, "Fine-Grained Formal Specification and Analysis of Buddy Memory Allocation in Zephyr RTOS", <em>
<u>IEEE 22nd International Symposium on Real-Time Distributed Computing (ISORC 2019)</u></em>, 7-9 May, 2019, Valencia, Spain, pp. 10-17.
</li>
<li>
<text class="paperlable">[SETTA 2019]</text>
Yu Zhang, <strong>Yongwang Zhao#</strong>, David Sanan, Lei Qiao, and Jinkun Zhang, "A Verified Specification of TLSF Memory Management Allocator using State Monads", <em>
<u>International Symposium on Software Engineering: Theories, Tools, and Applications (SETTA 2019)</u></em>, Nov. 27-29, 2019, Shanghai, China, pp. 122-138.
<a href="https://link.springer.com/content/pdf/10.1007/978-3-030-35540-1_8.pdf" target="_blank"><strong>[PDF download]</strong></a> (<em><strong>CCF C</strong></em>)
</li>
<li>
Shahbaz Ali, Hailong Sun, and <strong>Yongwang Zhao#</strong>, "Combining Model Learning and Model Checking to Analyze Java Libraries", <em>
<u>9th International Workshop on Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2019)</u></em>, Shenzhen, China, November 5, 2019, pp. 259-278.
</li>
<li>
Ke Jiang, David Sanan, <strong>Yongwang Zhao</strong>, Shuanglong Kan, Yang Liu, "A Formally Verified Buddy Memory Allocation Model", <em>
<u>24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019)</u></em>, 10-13 November 2019, Guangzhou, China, pp. 144-153. (<em><strong>CCF C</strong></em>)
</li>
<li>
<strong>赵永望</strong>等. “形式化方法的研究进展与趋势”. 中国计算机学会CCF 2017-2018中国计算机科学技术发展报告, 1-68, 2018. 机械工业出版社.
</li>
<!--
<li>
Jianwen Sun, Xiang Long, <strong>Yongwang Zhao#</strong>, "A Verified Capability-based Model for Information Flow Security with Dynamic Policies",
<em><u>IEEE Access Journal</u></em>, Volume 6, April 2018, pp. 16359 - 16407 (SCI影响因子3.224) <a href="papers/Access2018.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
-->
<!--
<li>
Feng Zhang, <strong>Yongwang Zhao</strong>#, Wensheng Niu, DianfuMa, "Formal Verification of Behavioral AADL Models By Stateful Timed CSP",
<em><u>IEEE Access Journal</u></em>, Volume 5, December 2017, pp. 27421 - 27438 (SCI影响因子3.224) <a href="papers/Access2017.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
-->
<li>
<strong>赵永望</strong>, 冯新宇, "防黑客编程", <em><u>中国计算机学会通讯</u></em>, 第13卷, 第10期, 2017年10月 (译文).
</li>
<li><strong>Yongwang Zhao</strong>, David Sann, Fuyuan Zhang, Yang Liu, "Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement", <em><u>IEEE Transactions on Industrial Informatics</u></em>, Volume 12, No. 4, August, 2016, pp. 1321 - 1331. (<em>影响因子 8.785</em>) <a href="papers/TII2016.pdf" target="_blank"><strong>[PDF download]</strong></a> </li>
<li>
<strong>Yongwang Zhao</strong>, David Sanan, Fuyuan Zhang, Yang Liu, "High-Assurance Separation Kernels: A Survey on Formal Methods", CoRR abs/1701.01535 (2017) <a href="https://arxiv.org/pdf/1701.01535.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<!--
<li>
Shuxian Zhang, <strong>Yongwang Zhao</strong>#, Yan Teng, Feng Zhang, "Model-driven Development and Formal Analysis of A GNC Telemetry System", <u>International Journal of Software and Informatics</u> (To appear, recommended by FMAC 2017).
</li>
-->
<li>
<strong>赵永望</strong>, 胡春明, "基于公式的软件调试", <em><u>中国计算机学会通讯</u></em>, 第12卷, 第9期, 2016年9月 (译文).
</li>
<!-- <li><strong>Yongwang Zhao</strong>, David Sann, Fuyuan Zhang, Yang Liu, "Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication", CoRR abs/1510.05091 (2015) <a href="http://arxiv.org/abs/1510.05091" target="_blank">[Link]</a></li>-->
<li>David Sanan, Yang Liu, <strong>Yongwang Zhao</strong>, Zhenchang Xing, Mike Hinchey, "Verifying FreeRTOS' Cyclic Doubly Linked List Implementation: From Abstract Specification to Machine Code", <em>20th International Conference on Engineering of Complex Computer Systems (ICECCS 2015)</em>, December 9-12, Gold Coast, Australia (<em><strong>CCF C</strong></em>) .</li>
<li>
Kun Cheng, Yuebin Bai, <strong>Yongwang Zhao</strong>#, Yao Ma, Duo Lu, Yuanfeng Peng, Minxuan Zhou, " HV2M: A novel approach to boost inter-VM network performance for Xen-based HVMs ", <em><u>Journal of Systems and Software</u></em>, Volume 114, April 2016, pp.54–68. (<strong><em>CCF B</em></strong>)
</li>
<li>Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali,Kai Hu, <strong>Yongwang Zhao</strong>, Dianfu Ma, "Towards a Verified Compiler Prototype for the Synchronous Language SIGNAL", <u><em>Frontiers of Computer Science</em></u>, Volume 10, Issue 1 (February 2016), pp 37–53, Springer (<strong><em>CCF B</em></strong>) . </li>
<li>
杨志斌,<strong>赵永望</strong>,黄志球, 胡凯,马殿富,Jean-Paul BODEVEIX, Mamoun FILALI, "基于同步语言的的时间可预测多线程代码生成方法", <em><u>软件学报</u></em>, 2016, 27(3): 611-632.</li>
<li>
杨志斌,胡凯,<strong>赵永望</strong>,马殿富,Jean-Paul BODEVEIX,"基于时间抽象状态机的AADL模型验证", <u><em>软件学报</em></u>, 2015, 26(2): 202-222.</li>
<li>
<strong>Yongwang Zhao</strong>, Zhuqing Li, Hualei Shen, Dianfu Ma, "Development of Global Specification for Dynamically Adaptive Software",
<em>Computing</em>, Volume 95, Issue 9 (2013), pp. 785-816, Springer (<strong><em>SCI-Indexed</em></strong>)
<a href="papers/Comp2013.pdf" target="_blank"><strong>[PDF download]</strong></a>.</li>
<li>
Jing Li, <strong>Yongwang Zhao</strong>, Hailong Sun, Zibin Zheng, Dianfu Ma, "DH4SS: A Distributed Heuristic for QoS-Based Service Selection", <em>International Journal of Web and Grid Services (IJWGS), </em>Vol.7, No.4, 2011, pp.388-409 (<em><strong>Top journal in web services, SCI-Indexed</strong></em>) </li>
<li>
Hualei Shen, Dianfu Ma, <strong>Yongwang Zhao</strong>#, Hailong Sun, Sujun Sun, Rongwei Ye, Lei Huang, Bo Lang, Yan Sun, "MIAPS: a web-based system for remotely accessing and presenting medical images", <em>Computer Methods and Programs in Biomedicine</em>, Volume 113, Issue 1 (January, 2014), pp. 266–283, Elsevier(<strong><em>SCI-Indexed</em></strong>). </li>
<li>
<strong>Yongwang Zhao</strong>, Chunyang Hu, Hualei Shen, Dianfu Ma, Xuan Li, Yonggang Huang, "A Hierarchical Organization Approach of Multi-dimensional Remote Sensing Data for Lightweight Web Map Services", <em>Earth Science Informatics</em>, Volume 5, Issue 1 (2012), pp. 61-75, Springer (<strong><em>SCI-Indexed</em></strong>). </li>
<li>
Hao, Zeng, Dianfu Ma, <strong>Yongwang Zhao</strong>, Zhuqing Li, "PBA4WSSP: A Policy-Based Architecture for Web Services Security Processing", <em>Service Oriented Computing and Applications</em>, Volume 8, Issue 1 (March, 2014), pp. 55 - 72, Springer (<em><strong>CCF C</strong></em>). </li>
<li>Bingyang Zhao, <strong>Yongwang Zhao</strong>, Dianfu Ma, "A Constraint Mechanism for Dynamic Evolution of Service Oriented Systems", <em>15th IEEE symposium on object/component/service-oriented realtime distributed computing(ISORC 2012)</em>, IEEE Computer Society, April 11-13, 2012, Shenzhen, China, pp.103-110. </li>
<li>Ying Wang, Dianfu Ma,<strong> Yongwang Zhao</strong>, Lu Zou, Xianqi Zhao, "Automatic RT-Java code generation from AADL models for ARINC653-based avionics software", <em>36th IEEE Computer Software and Applications Conference (COMPSAC 2012)</em>, IEEE Computer Society, July 16-20, 2012, Izmir, Turkey (<em><strong>CCF B</strong></em>) . </li>
<li>
Ying Wang, Dianfu Ma, <strong>Yongwang Zhao</strong>, "An AADL-based modeling method for ARINC653-based avionics software", <em>35th IEEE Computer Software and Applications Conference (COMPSAC 2011) </em>, IEEE Computer Society, July 18-22, 2011, Munich, German, pp.224-229 (<em><strong>CCF B</strong></em>) .</li>
<li>Zhuqing Li, Dianfu Ma, <strong>Yongwang Zhao</strong>, Jing Li, Qing Yang, "FSM4WSR: A Formal Model for Verifiable Web Service Runtime", Proceedings of 2011 IEEE Asia-Pacific Services Computing Conference (APSCC 2011), IEEE Computer Society, December 12 - 15, 2011, Jeju, Korea, pp.86-93.
</li>
</ol>
</div>
</div>
</div>
</div>
</div>
</div> <!-- End first group -->
</div>
</div> <!-- End of tiles -->
<footer data-load="footer.html">
</footer>
</div>
<script src="js/hitua.js"></script>
</body>
</html>