宋富课题组高鹏飞（博）于2019年4月赴捷克布拉格参加ETAPS2019并做口头汇报

ETAPS 2019于2019年4月6日至11日在捷克首都布拉格举行。ETAPS是欧洲软件理论与实践的联合会议，是欧洲主要的软件科学研究的学术会议。由ESOP，FASE，FoSSaCS，POST和TACAS这五个年度会议以及一些workshop构成。ETAPS也是CCF-B类推荐会议。此次我们的工作作为research paper被ETAPS中的TACAS（International Conference on Tools and Algorithms for the Construction and Analysis of Systems）会议所接收。今年TACAS共收到164篇投稿，共接收了50篇论文。我们的论文是唯一一篇以大陆单位为第一完成单位的research paper。

在这篇论文中，我们提出一种结合类型推导和模型计数的方法，用于验证防御侧信道攻击程序是否安全。我们的方法可以直接在算术程序上进行验证。同时如果程序不安全，我们也提供一种衡量信息泄露量的方法。为了提高效率，我们也提出了一些启发式策略，这些方法在实验中被证明是行之有效的。值得一提的是，我们在验证防御侧信道攻击程序的一些工作，近日也被CCF-A类推荐期刊TOSEM接收。

4月6日和7日是两天workshop，我主要参加了Mooly Fest Workshop和Mentoring Workshop。8日是Main Conference的第一天，首先大会主席介绍了今年ETAPS的论文接收情况等会议信息，接着就是精彩的keynote环节和各个学者的报告。在8日下午，我就我们的工作做了30分钟的口头报告，并一一回答了观众们的提问。图1为报告现场。

图1报告现场

8日晚上同时进行了Main Conference的接待以及墙贴展示环节。参加墙贴环节不仅能欣赏到设计精致的posters，也能和研究者们面对面交流。我同来自爱丁堡大学的Chao Peng讨论了如何评估GPU程序的测试集好坏，他在论文中提出了一些评价指标并通过人为干预线程的执行顺序来发现程序中错误。GPU程序的测试类似传统并发程序的测试，但又有不同，这是个有意义也有意思的工作。我也同来自Paderborn University的Philipp Schubert讨论了他的C/C++静态分析框架相关的工作，他基于LLVM实现了C/C++程序的过程间分析，实现了经典的过程间分析算法IFDS/WPDS等。作为一个程序分析工具，我比较关心该工具有没有用到真实世界中C/C++程序，并做一些有趣的应用。Philipp表示相关的工作已经在投。图2为该工作的墙贴。

图2 C/C++过程间分析框架

另一件比较难忘的事是我被选为大会的学生志愿者，这也是我第一次体验学术会议的志愿者。我主要负责帮助演讲者播放slides，在提问环节传递话筒等。虽然工作简单，但是能帮助大会顺利举办也很有意义。