vas-group-imperial/venus

Venus is a state-of-the-art sound and complete verification toolkit for Relu-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties. Venus implements a MILP-based verification method whereby it leverages dependency relations between the ReLU nodes to prune the search tree that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting. Venus is developed at the Verification of Autonomous systems Lab at the Department of Computing, Imperial College London for the purposes of the Assured Autononmy Project.