We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).
@inproceedings{mueller2023abstract, title = {Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks}, url = {https://doi.org/10.1145/3591252} doi = {10.1145/3591252} booktitle = {{PLDI} '23: 44nd {ACM} {SIGPLAN} International Conference on Programming Language Design and Implementation, Orlando, Florida, United States June 17-21, 2023}, publisher = {ACM}, author = {Mark Niklas Müller and Marc Fischer and Robin Staab and Martin T. Vechev}, year = {2023}}