2021年1月6日下午，在理科大楼B211召开了“自主可控、安全可靠”可信软件研究生创新学术分享会。beat365手机中文官方网站副院长陈铭松（主持工作）、软件科学与技术系系主任张民、嵌入式软件与系统系系主任缪炜恺、密码与网络安全系系副主任张磊担任点评专家。6位研究生代表分享了各自最新的学术成果。本次活动由张民副教授主持。

学术分享会现场，线上同步直播

2017级博士生刘富康同学在线上分享了在Crypto 2020上发表的论文《Automatic Verification of Differential Characteristics: Application to Reduced Gimli》。该论文主要介绍如何构建差分路线有效性自动化检测模型。其主要思想是在模型中同时考虑差分传播以及值传播。利用该模型，对NIST轻量级密码算法竞赛的第二轮候选算法Gimli进行了分析。

2017级博士生乔琪同学分享了在IEEE SECON 2020上发表的论文《Hybrid Intrusion Detection Mechanisms for Integrated Electronic Systems》。该论文主要介绍面向基于1553B总线的综合电子系统的入侵检测方案。其主要思想是针对1553B总线协议特殊的通信机制，对总线上的周期性消息和非周期性消息分别提出了序列检测和决策树检测算法，并通过仿真实验证明所提出的方案达到了实时、准确的检测效果。

乔琪同学分享学术成果

2016级博士生张枨宇同学分享了在PLDI 2020以及OOPSLA 2020上发表的与SMT求解器测试相关的工作，分别介绍了基于构造预期输出的语义融合方法，以及基于差异测试的公式变异方法。这一系列工作共在目前最好的SMT求解器Z3和CVC4中找出千余个缺陷，其中有数百个严重的求解错误缺陷。该系列工作提升了目前SMT求解器的可靠性，在国际上受到了广泛的关注。

张枨宇同学分享学术成果

2019级博士生胡铭同学分享了在DAC 2019上发表的论文《Sample-Guided Automated Synthesis for CCSL Specifications》。该论文提出了一种基于SKETCH的时间约束规约语言（CCSL）的综合方法，将CCSL的综合问题转化为sketching问题，帮助设计人员生成满足预期时间行为的CCSL规约。

胡铭同学分享学术成果

2017级博士生秦旭东同学介绍了在TACAS2020上发表的论文《Verifying Quantum Communication Protocols with Ground Bisimulation》中的工作。论文的主要内容是关于通过检测量子基互模拟来判断量子程序的实现与需求规约之间是否等价，以此验证量子程序的正确性。为此该论文设计并实现了两个on-the-fly算法，分别用于检测两个由量子CCS编写的量子程序之间的强基互模拟以及弱基互模拟。并且基于算法的实现开发了自动化的验证工具QBisim，用于验证各种量子协议，例如量子隐态传输协议、量子密钥分发协议、BB84量子密钥分配方案等。

秦旭东同学分享学术成果

2016级博士生王露同学在CCF-A会议KDD发表论文《Supervised reinforcement learning with recurrent neural network for dynamic treatment recommendation》，被引52次，被下载2598次。该论文解决了医疗领域动态辅助治疗问题，即如何实时推荐合适的治疗方案给医生用作辅助医生治疗病人。解决问题的思想在于同时利用医生的监督信号和病人不同时刻的存活信号作为奖赏信号，利用强化学习算法基于历史治疗数据搜索出更优的治疗方案。该技术在离线的800个病人数据中测试，获得了比原始数据更低的估计死亡率。

王露同学分享学术成果

四位专家围绕研究生代表的科研成果展开了点评与讨论，与会学生通过线上会议室留言及现场提问的方式，积极学习研究生代表的成功经验。点评专家陈铭松教授总结了2020年研究生学术创新的总体情况，并激励所有学生在科研上要“不惧困难、勇于尝试、敢于突破”。

点评专家陈铭松教授激励研究生科研创新

本次活动采用现场互动、线上直播的形式，吸引了众多学生参加。通过海报展示、创新学术分享，向全院师生展示2020年研究生获得的标杆性研究成果，激发了研究生对前沿技术的进一步探索，用辩证思维深入思考及研究，以推动全院高水平学术氛围的形成，为实现“培养学科相关领域的高端人才、为国家新工科发展提供优秀人才保障”的目标搭建平台。

研究生参观学术成果海报