Automated Safety Verification of Programs Invoking Neural Networks

被引：8

作者：

Christakis, Maria ^{[1
,2
]}

Eniser, Hasan Ferit ^{[1
,2
]}

Hermanns, Holger ^{[3
,7
]}

Hoffmann, Joerg ^{[3
]}

Kothari, Yugesh ^{[1
,2
]}

Li, Jianlin ^{[3
,4
,8
]}

Navas, Jorge A. ^{[5
]}

Wuestholz, Valentin ^{[6
]}

机构：

[1] MPI SWS, Kaiserslautern, Germany

[2] MPI SWS, Saarbrucken, Germany

[3] Saarland Univ, Saarland Informat Campus, Saarbrucken, Germany

[4] Chinese Acad Sci, Inst Software, SKLCS, Beijing, Peoples R China

[5] SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA

[6] ConsenSys, Kaiserslautern, Germany

[7] Inst Intelligent Software, Guangzhou, Peoples R China

[8] Univ Chinese Acad Sci, Beijing, Peoples R China

来源：

COMPUTER AIDED VERIFICATION (CAV 2021), PT I | 2021年 / 12759卷

基金：

美国国家科学基金会;

关键词：

ABSTRACT DOMAIN; MODEL CHECKING; CRASH;

D O I：

10.1007/978-3-030-81685-8_9

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：201 / 224

页数：24

共 70 条

[1]

Albarghouthi Aws, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P672, DOI 10.1007/978-3-642-31424-7_48

[2]

Alshiekh M, 2018, AAAI CONF ARTIF INTE, P2669

[3]

[Anonymous], 2016, ARXIV160704311

[4] ET-RNN: Applying Deep Learning to Credit Loan Applications [J].

Babaev, Dmitrii ;

Savchenko, Maxim ;

Tuzhilin, Alexander ;

Umerenkov, Dmitrii .

KDD'19: PROCEEDINGS OF THE 25TH ACM SIGKDD INTERNATIONAL CONFERENCCE ON KNOWLEDGE DISCOVERY AND DATA MINING, 2019, :2183-2190

[5]

Baier C., 2020, LNCS, V12641, P83

[6] LEARNING TO ACT USING REAL-TIME DYNAMIC-PROGRAMMING [J].

BARTO, AG ;

BRADTKE, SJ ;

SINGH, SP .

ARTIFICIAL INTELLIGENCE, 1995, 72 (1-2) :81-138

[7] Generating tests from counterexamples [J].

Beyer, D ;

Chlipala, AJ ;

Henzinger, TA ;

Jhala, R ;

Majumdar, R .

ICSE 2004: 26TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2004, :326-335

[8]

Beyer D, 2012, P ACM SIGSOFT 20 INT, DOI DOI 10.1145/2393596.2393664

[9]

Biere A, 1999, LECT NOTES COMPUT SC, V1579, P193

[10] A static analyzer for large safety-critical software [J].

Blanchet, B ;

Cousot, P ;

Cousot, R ;

Feret, J ;

Mauborgne, L ;

Miné, A ;

Monniaux, D ;

Rival, X .

ACM SIGPLAN NOTICES, 2003, 38 (05) :196-207

← 1 2 3 4 5 6 7 →