CAV 之往事可追忆

19 号，第 32 届 CAV （Computer Aided Verification）会议正式于线上举行，会议致力于硬件和软件系统的计算机辅助形式化分析方法的理论和实践的进步，涵盖从实用的验证工具以及实现这些工具所需的算法和技术。

此届大会共录取了 65 篇论文。来自 Facebook 的首席研究员 David Cali、DeepMind 的首席科学家兼团队负责人 Pushmeet Kohli 将带来有关区块链、机器学习等相关的主题演讲。

今年的大会可谓是精彩纷呈，好奇心爆棚的你是否想了解 CAV 的过去会是怎样的呢？

那请跟随着 AMiner 一起来找寻属于 CAV 的五年记忆吧！

通过对 AMiner 平台中 CAV 2015-2019 这五年来收录论文数据的挖掘，从词云可以看出，CAV 的关键词主要集中在 Markov Decision Processes、Chemical Reaction Networks、Program Repair、Hybrid Systems、Abstract Interpretation 等方向。

通过对 2015-2019 这五年来接收论文中所有学者信息的提取，可以看出，CAV 的投稿学者以男性为主导，占比 90.35%。从学者分布情况来看，投稿学者主要来自美国、澳大利亚、英国，分别占比 41.73%、8.27%，7.55%，中国学者以 5.39% 的占比排名第六。

从投稿学者发表所属机构来看，五年来在 CAV 会议中，牛津大学以 9 篇论文数量排在首位，奥地利科技大学和斯坦福大学以 5 篇位列第二。而就引用数量而言，斯坦福大学以 2890 的引用量排名第一，德国亚琛工业大学以 776 的引用量位列第二，伊利诺伊大学香槟分校列于第三，拥有 112 的引用量。

2015-2019五年间高引论文TOP10

1. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
作者：Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer

被引用量：578

2. Safety Verification of Deep Neural Networks
作者：Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu

被引用量：394

引用量排名前二的论文均是对神经网络的防御、验证问题的探讨。高引 No.1 的论文来自斯坦福大学，论文提出了一种用于神经网络错误检测的新算法 Reluplex。Reluplex  将线性编程技术与 SMT（可满足性模块理论）求解技术相结合，其中神经网络被编码为线性算术约束。论文的核心观点就是避免数学逻辑永远不会发生的测试路径，这允许测试比以前更大的数量级的神经网络。Reluplex 可以在一系列输入上证明神经网络的属性，可以测量可以产生虚假结果的最小或阈值对抗性信号。高引 No.2 的论文来自牛津大学，论文也是提出希望基于可满足性模理论对神经网络的鲁棒性做一些验证。

3. A storm is Coming: A Modern Probabilistic Model Checker
作者：Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk

被引用量：194

4. The SeaHorn Verification Framework
作者：Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas

被引用量：170

5. SMT-Based Model Checking for Recursive Programs
作者：Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki

被引用量：136

6. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool
作者：Christian Dehnert, Sebastian Junges, Nils Jansen,Florian Corzilius, Matthias Volk,Harold Bruintjes, Joost-Pieter Katoen, Erika Ábrahám

被引用量：96

7. OptiMathSAT: A Tool for Optimization Modulo Theories
作者：Roberto Sebastiani, Patrick Trentin

被引用量：90

8. From Invariant Checking to Invariant Inference Using Randomized Search

作者：Rahul Sharma, Alex Aiken

被引用量：84

9. Algorithms for Model Checking HyperLTL and HyperCTL
作者：Bernd Finkbeiner, Markus N. Rabe, César Sánchez

被引用量：83

10. Qlose: Program Repair with Quantitative Objectives
作者：Loris D'Antoni, Roopsha Samanta, Rishabh Singh

被引用量：74

2015-2019五年间高引学者TOP10

No.1 Clark Barrett

被引用量：733

Clark Barrett 于 2016 年 9 月加入斯坦福大学，担任计算机科学专业的副教授，他的专长是约束求解及其在系统验证和安全性方面的应用。他是 ACM 杰出科学家。

No.2 Guy Katz

被引用量：656

Guy Katz 是耶路撒冷希伯来大学计算机科学与工程学院的助理教授。研究重点是应用形式化方法来创建可靠合适的软件，他对使用机器学习的组件（例如神经网络）进行形式验证的系统特别感兴趣。

No.3 Mykel Kochenderfer

被引用量：616

Mykel Kochenderfer 是斯坦福大学航空与航天专业的助理教授。他是斯坦福智能系统实验室（SISL）的负责人，致力于设计鲁棒决策系统的高级算法和分析方法，尤其关注的是用于空中交通管制，无人驾驶飞机和其他航空航天应用的系统.

No.3 David Dill 

被引用量：616

Dill 现为斯坦福大学的名誉教授，已经退休，目前是 Facebook 的区块链技术研究员。他对系统设计的验证技术感兴趣。他还从事异步电路验证和综合以及硬实时系统的验证方法方面的研究。

想找寻关于CAV的更多记忆吗？请移步：

https://www.aminer.cn/conference/53a7279620f7420be8b93844

想要了解更多学术进展、前沿科技资讯，参与学术头条每日话题讨论，可以扫描二维码或搜索AMiner308添加学术君微信，对学术君说: “我想进读者群”, 即可进入读者群，不定期发福利~

点击 阅读原文 ，查看更多精彩！

喜欢本篇内容，请 分享、点赞、在看