Automated Safety Verification of Programs Invoking Neural Networks
Automated Safety Verification of Programs Invoking Neural Networks
复制标题
DOI：
10.1007/978-3-030-81685-8_9
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
M. Christakis;Hasan Ferit Eniser;H. Hermanns;J. Hoffmann;Yugesh Kothari;Jianlin Li;J. Navas;Valentin Wüstholz
中科院分区：
文献类型：
--
作者：
M. Christakis;Hasan Ferit Eniser;H. Hermanns;J. Hoffmann;Yugesh Kothari;Jianlin Li;J. Navas;Valentin Wüstholz
最先进的程序分析技术还不能有效地验证异类系统的安全属性，即具有使用不同技术实现的组件的系统。尽管神经网络在许多应用领域扮演着广受赞誉的创新驱动力的角色，但调用神经网络的程序准确地指出了这一缺陷。本文对程序与神经网络相互作用的系统进行了系统级性质的验证。我们的技术提供了程序和神经网络分析的紧密双向集成，并在基于抽象解释的通用框架中形式化。我们在一个广泛使用的受限自动驾驶基准的26个变体上评估了它的有效性。
State-of-the-art program-analysis techniques are not yet able to effectively verify safety properties of heterogeneous systems, that is, systems with components implemented using diverse technologies. This shortcoming is pinpointed by programs invoking neural networks despite their acclaimed role as innovation drivers across many application areas. In this paper, we embark on the verification of system-level properties for systems characterized by interaction between programs and neural networks. Our technique provides a tight two-way integration of a program and a neural-network analysis and is formalized in a general framework based on abstract interpretation. We evaluate its effectiveness on 26 variants of a widely used, restricted autonomous-driving benchmark.