Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 14:00 - 14:25 at Foyer - Session 3 Chair(s): Eunsuk Kang

Artificial neural networks (ANN) have displayed considerable utility in a wide range of applications such as image processing, character and pattern recognition, self-driving cars, evolutionary robotics, and non-linear system identification and control. While ANNs are able to carry out complicated tasks efficiently, they are susceptible to unpredictable and errant behavior due to irregularities that emanate from their complex non-linear structure. As a result, there have been reservations about incorporating them into safety-critical systems. In this paper, we propose a reachability analysis method for feed- forward neural networks (FNN) that employ rectified linear units (ReLUs) as activation functions. The crux of our approach relies on three reachable-set computation algorithms, namely exact schemes, lazy-approximate schemes, and mixing schemes. The exact scheme computes an exact reachable set for an FNN, while the lazy-approximate and mixing schemes generate an over-approximation of the exact reachable set. All schemes are designed efficiently to run on parallel platforms to reduce the computation time and enhance the scalability. Our methods are implemented in a MATLAB toolbox called, NNV, and is evaluated using a set of benchmarks that consist of realistic neural networks with sizes that range from tens to a thousand neurons. Notably, NNV successfully computes and visualizes the exact reachable sets represented as a union of tens to hundreds of polyhedra, of the real-world ACAS Xu deep neural networks (DNNs) in the new generation of Airborne Collision Avoidance System X.

Mon 27 May
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 15:30: Session 3FormaliSE at Foyer
Chair(s): Eunsuk KangCarnegie Mellon University
14:00 - 14:25
Full-paper
Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks
FormaliSE
Hoang-Dung TranVanderbilt University, Patrick MusauVanderbilt University, Diego Manzanas LopezVanderbilt University, Xiao Dong YangVanderbilt University, Luan NguyenUniversity of Pennsylvania, Weiming XiangVanderbilt University, Taylor T JohnsonVanderbilt University
14:25 - 14:40
Short-paper
Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata
FormaliSE
Maxime CordySnT, University of Luxembourg, Axel Legay, Sami LazregVisteon Electronics and Universite Cote d Azur, Philippe ColletUniversity of Nice
14:40 - 15:05
Full-paper
Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP
FormaliSE
Jan PedersenUniversity of Nevada Las Vegas, Kevin ChalmersEdinburgh Napier University
15:05 - 15:30
Full-paper
A Generalized Program Verification Workflow Based on Loop Elimination and SA Form
FormaliSE
Cláudio Belo LourençoLRI, Université Paris-Sud & INRIA Saclay, Maria João FradeHASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa PintoHASLab/INESC TEC & Universidade do Minho, Portugal