FormaliSE 2025
Sun 27 - Mon 28 April 2025 Ottawa, Ontario, Canada
co-located with ICSE 2025

This program is tentative and subject to change.

Sun 27 Apr 2025 12:00 - 12:30 at 203 - Session 1 - Formal Methods and Autonomous Systems

Deep neural networks (DNNs) have shown impressive performance in computer vision tasks, driven by the availability of large datasets and advanced deep learning techniques. This success has prompted the formal methods community to explore ways of evaluating and improving the reliability and correctness of these models. These verification efforts, however, have primarily focused on neural networks that process image or feature data, overlooking architectures designed for video data. This oversight hinders the deployment of advanced computer vision techniques for safety-critical tasks such as video surveillance, self-driving, and industrial automation, where reliable performance is required. In this work, we develop a formal verification approach to video classification tasks. This includes a novel abstract convex set definition that can represent video data (image data with a temporal component), as well as new reachability methods for layers commonly used by video classification neural networks such as three-dimensional convolutional and three-dimensional pooling layers. Additionally, we construct 3 datasets: Zoom In MNIST, Zoom Out MNIST, and GTRSB Video. These are built upon common datasets from image classification in the formal methods community (MNIST, GTSRB). These three datasets and the ST-MNIST dataset are used to train a video classification neural network and then formally verify their robustness against L$_{\infty}$ norm perturbations. Our results show the scalability of our approach to different input sizes and where the main challenges in this domain are.

This program is tentative and subject to change.

Sun 27 Apr

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Session 1 - Formal Methods and Autonomous Systems Research Track at 203
11:00
30m
Talk
CPS Falsification using Autoencoded Input Models
Research Track
Youssef Zahar University of Minnesota, Sanjai Rayadurgam University of Minnesota
11:30
30m
Talk
Modeling Language for Scenario Development of Autonomous Driving Systems
Research Track
Toshiaki Aoki JAIST, Takashi Tomita JAIST, Tatsuji Kawai Kochi University, Daisuke Kawakami Mitsubishi Electric Corporation, Nobuo Chida Mitsubishi Electric Corporation
12:00
30m
Talk
Robustness Verification of Video Classification Neural Networks
Research Track
Samuel Sasaki Vanderbilt University, Preston K. Robinette Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Taylor T Johnson Vanderbilt University