Interval Image Abstraction for Verification of Camera-Based Autonomous Systems
P. Habeeb, Deepak D’Souza, Kamal Lodaya, Pavithra Prabhakar · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2024
We propose an abstraction-refinement-based algorithm for the problem of verifying the safety of a camera-based autonomous system in a synthetic 3D-scene, based on the notion of interval images. An interval image is an abstract data structure that represents a set of images in a 3D-scene. We give a computer graphics style rendering algorithm to efficiently compute interval images from a given region. Our proposed abstraction-refinement algorithm leverages recent abstract interpretation tools for neural networks. We have implemented and evaluated the proposed technique on complex 3D-scenes, demonstrating its effectiveness and scalability in comparison with earlier techniques.