Deep learning has emerged as an effective approach for creating
modern software systems, with neural networks often surpassing
hand-crafted systems. Unfortunately, neural networks are known
to suffer from various safety and security issues. Formal
verification is a promising avenue for tackling this difficulty, by
formally certifying that networks are correct. We propose an SMT-based 
technique for verifying binarized neural networks
- a popular kind of neural network, where some weights have been
binarized in order to render the neural network more memory and
energy-efficient, and quicker to evaluate. One novelty of our
technique is that it allows the verification of neural networks that
include both binarized and non-binarized components. Neural network
verification is computationally very difficult, and so we propose
here various optimizations, integrated into our SMT procedure as
deduction steps, as well as an approach for parallelizing
verification queries. We implement our technique as an extension to
the Marabou framework and use it to evaluate the approach on popular
binarized neural network architectures.

An SMT-Based Approach for Verifying Binarized Neural Networks

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme