2020年7月29日，第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中，引用量排名前二的论文均是对神经网络的防御、验证问题的探讨。高引No.1的论文来自斯坦福大学，论文提出了一种用于神经网络错误检测的新算法Reluplex。
Reluplex将线性编程技术与SMT（可满足性模块理论）求解技术相结合，其中神经网络被编码为线性算术约束。论文的核心观点就是避免数学逻辑永远不会发生的测试路径，这允许测试比以前更大的数量级的神经网络。Reluplex可以在一系列输入上证明神经网络的属性，可以测量可以产生虚假结果的最小或阈值对抗性信号。高引No.2的论文来自牛津大学，论文也是提出希望基于可满足性模理论对神经网络的鲁棒性做一些验证。
2015-2019五年间高引学者TOP10中，No.1 Clark Barrett于2016年9月加入斯坦福大学，担任计算机科学专业的副教授，他的专长是约束求解及其在系统验证和安全性方面的应用。他是ACM杰出科学家。No.2 Guy Katz是耶路撒冷希伯来大学计算机科学与工程学院的助理教授。
研究重点是应用形式化方法来创建可靠合适的软件，他对使用机器学习的组件（例如神经网络）进行形式验证的系统特别感兴趣。No.3 Mykel Kochenderfer是斯坦福大学航空与航天专业的助理教授。他是斯坦福智能系统实验室（SISL）的负责人，致力于设计鲁棒决策系统的高级算法和分析方法，尤其关注的是用于空中交通管制，无人驾驶飞机和其他航空航天应用的系统。
No.3 David Dill现为斯坦福大学的名誉教授，已经退休，目前是Facebook的区块链技术研究员。他对系统设计的验证技术感兴趣。他还从事异步电路验证和综合以及硬实时系统的验证方法方面的研究。