Talk by Edoardo Manino, (University of Manchester).
Safety-critical systems with neural network components require strong guarantees. While existing verification techniques have shown great progress towards this goal, they mostly reason on high-level abstractions of neural networks. As soon as we consider the finite precision of machine arithmetic, and the specific software implementation of neural networks, the associated verification problem becomes harder. In this talk, we will present the advantages and shortcomings of reasoning on neural networks at the bit-precise level for verification and synthesis purposes.