-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnews.html
414 lines (335 loc) · 19.4 KB
/
news.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 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>
.container {
width: 1040px;
}
.news_icon {
display: block;
width: 150px;
font-size: 40px;
float: left;
margin-right: 10px;
}
.news_data {
display: block;
padding: 0;
margin: 0;
margin-left: 160px;
min-width: 200px;
position: relative;
}
.news_data2 {
display: block;
padding: 0;
margin: 0;
margin-left: 0;
min-width: 200px;
position: relative;
}
</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="tile-area no-padding clearfix">
<div class="tile-group no-margin no-padding clearfix" style="width: 100%">
<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> News </a></li>
<!--<li><a href="#_page_2">Personal News</a></li>
<li><a href="#_page_3">Tech News</a></li>-->
</ul>
<div class="frames">
<div class="frame" id="_page_1">
<div class="listview-outlook">
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2021-9-24]</a>
本人当选中国计算机学会(CCF)杰出会员，详见<a href="https://www.ccf.org.cn/Membership/Individual_member/" target="_blank">CCF官网</a>。
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2021-7-31]</a>
<a href="https://www.acmturc.com/" target="_blank">ACM中国图灵大会(ACM TURC 2021)</a>召开，我受邀在“高可信软件技术论坛”做主题演讲。
<a href="https://c.eqxiu.com/s/TdocXW68?bt=yxy&eqrcode=1&share_level=1&from_user=20210718c17657fd&from_id=286b10eb-6&share_time=1627013380309" target="_blank"><strong>详见微信</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2021-7-1]</a>
我们编写的书籍《函数式程序设计与证明》已发布，内容不断更新中......
<a href="https://www.yuque.com/zhaoyongwang/fpp" target="_blank"><strong>详见书籍网站</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2021-5-9]</a>
受邀在 2021全国大学生计算机系统能力大赛-操作系统设计大赛 做技术报告：操作系统正确性及其验证技术。
<a href="https://os.educg.net/" target="_blank"><strong>详见主页</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2021-1-30]</a>
受邀在载人航天软件工程未来发展专家研讨会 做技术报告：形式化验证-现状与展望。
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2020-12-30]</a>
作为发起人之一，发起成立TPChina定理证明开放社区，
<a href="https://tpchina.github.io/" target="_blank"><strong>详见官网</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2020-11-25]</a>
受邀在Symposium on Dependable Software Engineering: Theories, Tools and Applications(SETTA 2020)做大会报告：Rely-guarantee Reasoning about Concurrent Reactive Systems: Framework, Languages Integration and Applications。
<a href="http://lcs.ios.ac.cn/setta2020/" target="_blank"><strong>详见主页</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[2020-11-21]</a>
受邀在CCF中国软件大会(Chinasoft2020)做学术报告：操作系统安全形式化验证技术与应用。
<a href="http://chinasoft2020.cqu.edu.cn/" target="_blank"><strong>详见主页</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[Oct. 24, 2020]</a>
受邀为中国计算机大会CNCC2020做学术报告：安全攸关操作系统形式化验证-技术与应用实践。
<a href="http://cncc2020.ccf.org.cn/" target="_blank"><strong>详见主页</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[Oct. 16, 2020]</a>
受邀为计算机学会CCF软件前沿系列讲座做学术报告：操作系统并发内存管理的形式化验证技术。
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[June 22, 2020]</a>
受邀为计算机学会CCF新基建安全技术系列讲座做学术报告：安全关键软件形式化方法——概念、技术与工业应用。
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[December 23, 2019]</a>
经过3年的努力，本人参与研制的ARINC 653新版标准正式发布。该标准委员会由美国波音公司和法国空客公司担任主席，包括霍尼韦尔、GE航空、法国泰雷兹、美国柯林斯，以及操作系统厂商风河、绿山等联合编写。
<a href="https://www.aviation-ia.com/products/653p1-5-avionics-application-software-standard-interface-part-1-required-services" target="_blank"><strong>see webpage</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[Nov. 30, 2019]</a>
受邀在FMAC2019青年学者论坛做学术报告：一种并发反应式系统组合验证的方法、实现及应用
<a href="https://basics.sjtu.edu.cn/news/fmac2019/program.html" target="_blank"><strong>see webpage</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[July 20, 2019]</a>
受邀在第二届中国核心技术创新发展峰会，做大会主题演讲《ARINC 653操作系统的形式化验证与安全认证》
<a href="http://gov.longhoo.net/2019/zwyw_0720/359309.html" target="_blank"><strong>见新闻网页</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[June 12, 2019]</a> Full paper accepted by <strong>FM 2019 (CCF B, top-tier in formal methods)</strong>. <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[April 17, 2019]</a> Full paper accepted by <strong>CAV 2019 (CCF A, top-tier in formal methods)</strong>. <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[Jan 2019]</a> Research paper published in <strong>IEEE Transactions on Dependable and Secure Computing (CCF A, top-tier in security)</strong>. <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[November 14, 2018]</a> 受法国空中客车公司邀请，到空客访问，并和空客航电产品、机载计算机、机载软件等部门的研发人员，讨论IMA分区操作系统、形式化方法、操作系统标准等成果和应用合作。
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[October 14, 2018]</a> 受邀在中国Linux内核开发者大会，做主题演讲《并发式伙伴内存管理C代码的形式验证》
<a href="http://www.ckernel.org/" class="fg-cobalt fg-hover-crimson" target="_blank"><strong>会议网站</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[September 15, 2018]</a> 受邀在中国软件工程研究与产业峰会，做主题演讲《物联网操作系统: 形式验证与安全认证》。演讲主题报告详见
<a href="https://mp.weixin.qq.com/s/1sf3JY4gOZl89Lo_yj2NxQ" class="fg-cobalt fg-hover-crimson" target="_blank"><strong>微信公众号文章</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[August 16, 2018]</a> 受邀在中国网络安全年会(CNCERT 2018)上，主持“物联网安全”分论坛，并做主题演讲《物联网操作系统: 形式验证与安全认证》。演讲主题报告，详见
<a href="https://mp.weixin.qq.com/s/1sf3JY4gOZl89Lo_yj2NxQ" class="fg-cobalt fg-hover-crimson" target="_blank"><strong>微信公众号文章</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<span class="list-title fg-darkRed">受邀成为Common Criteria(CC)的操作系统内核工作组成员，起草(多核)操作系统内核的security protection profile。</span>
<span class="list-subtitle" style="font-size:10pt">1/6/2018</span>
<!--<span class="list-remark" style="font-size:10pt">-->
<span class="panel-content margin10 fg-dark nlp nrp" style="font-size:10pt">
德国SYSGO公司发来Email，邀请我加入Common Criteria(CC)的操作系统内核工作组，起草(多核)操作系统内核的security protection profile。SYSGO是欧盟的盟产自主可控、高安全工业操作系统产品厂商，CC工作组的召集人，研制了PikeOS工业操作系统。<br/>
随着物联网、工业互联网、工业4.0的快速发展，CC在工业各领域发挥越来越重要的作用。德国、法国、美国、加拿大等工业发达国家，每年都有许多产品通过EAL 5+以上的CC安全认证，包括安全设备、工业控制系统、安全操作系统、数据库等。工业知名的操作系统，如绿山INTEGRITY-178、风河VxWorks Cert等，均符合CC EAL 6安全级别。EAL 5级以上，要求采用形式化方法进行产品开发，这正是我们目前重点研究方向之一。<br/>
我国由于种种原因尚没有工业产品，过CC安全认证。希望CC安全认证及相关技术，对国内工业，尤其是安全关键基础设施的发展，带来积极的影响。
</span>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[15 April 2018]</a> ARINC653操作系统标准委员会会议在法国Thales总部召开。波音、空客、霍尼韦尔、四大安全关键操作系统厂商(美国风河，绿山，DDC-I，德国SYSGO)、北京航空航天大学等单位参会。会上专题讨论了我们发表在IEEE Trans. on Dependable and Secure Computing的论文，对我们发现的安全漏洞进行确认，并相应修改标准。风河vxworks团队提出与我们合作的意愿。 <a href="https://mp.weixin.qq.com/s/geBK8NbMwbR0jYvYdTfxgA" class="fg-cobalt fg-hover-crimson" target="_blank"><strong>查看详情</strong></a> </li>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[10 April 2018]</a> Full paper accepted by International Symposium on Formal Methods (FM 2018) (CCF B, top tier in formal methods). <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[5 March 2018]</a> 我们在操作系统隔离内核方面的5篇研究论文，被著名的开源操作系统内核POK引为重要的参考文献。POK是法国几个大学开发的开源内核，已经被开发成商业操作系统JetOS，并应用到俄罗斯民航客机上。[<a href="https://pok-kernel.github.io/documentation/" class="fg-cobalt fg-hover-crimson" target="_blank">见POK官网</a>]
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[20 May 2017]</a> 参加在法国空客公司总部举行的ARINC653实时操作系统标准委员会会议，并正式成为委员会成员(中国首个成员)。
委员会聚集了国际上几乎所有航空航天制造商：两大整机厂商波音、空客；四大系统供应商GE航空、霍尼韦尔Honeywell、泰雷兹Thales、罗克韦尔Rockwell Colins；
四大操作系统软件供应商 风河WindRiver、绿山Green Hills、DDC-I、SYSGO(PikeOS)。[<a href="http://mp.weixin.qq.com/s/e4iRlQrnlOdc6h_SsJwWMQ" class="fg-cobalt fg-hover-crimson" target="_blank">查看详情</a>]
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[15 Feb 2017]</a> Journal paper accepted by IEEE Transactions on Dependable and Secure Computing (CCF A). <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[20 Dec 2016]</a> Full paper accepted by TACAS 2017 (CCF B, top tier in formal methods). <a href="publication.html" class="fg-cobalt fg-hover-crimson"><strong>See publication</strong></a>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
<a class="fg-cobalt fg-hover-crimson">[14 Oct 2016]</a> I received an acknowledgement email from Boeing and Airbus for our formal verification of ARINC 653 standard.
<span class="list-title fg-darkRed">实时操作系统标准研究成果得到美国波音公司等认可和接纳</span>
<span class="list-subtitle" style="font-size:10pt">14/10/2016</span>
<!--<span class="list-remark" style="font-size:10pt">-->
<span class="panel-content margin10 fg-dark nlp nrp" style="font-size:10pt">
我们收到来自美国波音公司Associate Fellow、ARINC653国际标准委员会主席的致谢邮件，对我们在ARINC653航空航天实时操作系统标准的研究成果表示认可，并将在ARINC653标准新版本中对存在的安全缺陷进行修复。<br/>
该项研究成果主要利用形式化方法对ARINC653标准进行完整的建模，并通过自动化手段完成1600多个定理的形式证明，最终发现了该标准的6个安全缺陷。相关成果已发表在ISSRE 2015国际会议（软件可靠性领域顶级会议）和IEEE Transactions on Industrial Informatics期刊。论文被ARINC653标准委员会高度关注， 2016年10月标准委员会年会上召开Workshop专门讨论上述论文的成果。最终，标准委员会确认ARINC653存在上述安全缺陷，并计划在其新版本中进行修复。<br/>
ARINC653标准是国际航空航天工业界实时操作系统的事实性标准，已有20年历史，被航空航天领域绝大多数实时操作系统所遵循，已应用到空客A380、波音787、F22、NASA猎户座飞船等。该标准委员会主席由来自波音和空客的两位资深专家担任，成员包括波音、空客、洛克希德马丁、GE航空、霍尼韦尔、达索航空、风河、法国泰雷兹等。
</span>
</div>
</div>
</div>
<div class="list">
<div class="list-content">
<div class="news_data2">
</div>
</div>
</div>
<ul>
</div>
</div>
</div>
<!--
<div class="frame" id="_page_2">
</div>
<div class="frame" id="_page_3">
</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>