Write a Blog >>
ASE 2021
Sun 14 - Sat 20 November 2021 Australia
Wed 17 Nov 2021 08:00 - 08:20 at Koala - Verification Chair(s): Nazareno Aguirre

DNN validation and verification approaches that are input distribution agnostic waste effort on irrelevant inputs and report false property violations. Drawing on the large body of work on model-based validation and verification of traditional systems, we introduce the first approach that leverages environmental models to focus DNN falsification and verification on the relevant input space. Our approach, DFV, automatically builds an input distribution model using unsupervised learning, prefixes that model to the DNN to force all inputs to come from the learned distribution, and reformulates the property to the input space of the distribution model. This transformed verification problem allows existing DNN falsification and verification tools to target the input distribution – avoiding consideration of infeasible inputs. Our study of DFV with 7 falsification and verification tools, two DNNs defined over different data sets, and 93 distinct distribution models, provides clear evidence that the counter-examples found by the tools are much more representative of the data distribution, and it shows how the performance of DFV varies across domains, models, and tools.

Wed 17 Nov

Displayed time zone: Hobart change

08:00 - 09:00
VerificationResearch Papers at Koala
Chair(s): Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina
08:00
20m
Talk
Distribution Models for Falsification and Verification of DNNs
Research Papers
Felipe Toledo , David Shriver University of Virginia, Sebastian Elbaum University of Virginia, Matthew B Dwyer University of Virginia
Pre-print
08:20
20m
Talk
SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools
Research Papers
Ugur Koc University of Maryland, College Park, Austin Mordahl The University of Texas at Dallas, Shiyi Wei The University of Texas at Dallas, Jeffrey S. Foster Tufts University, Adam Porter University of Maryland
08:40
20m
Talk
Efficient SMT-Based Model Checking for Signal Temporal Logic
Research Papers
Jia Lee POSTECH, Geunyeol Yu Pohang University of Science and Technology (POSTECH), Kyungmin Bae Pohang University of Science and Technology (POSTECH)