The SAIL group is actively maintaining a number of open-source software packages, including:
MCMAS is an open-source, OBDD-based symbolic model checker tailored to the verification of Multi-Agent Systems (MAS). MAS descriptions are given by means of ISPL (Interpreted Systems Programming Language) programs. ISPL is an agent-based, modular language inspired by interpreted systems, a popular semantics in MAS.
MCMAS supports a rich set of specifications, including CTL operators, epistemic operators, ATL, and notions pertaining to correct behaviour. Basic fairness conditions are supported. MCMAS enables the generation of counterexamples and witness executions for a wide range of specifications.
MCMAS can be downloaded here.
VErification of NeUral Systems 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. Further information can be found in the corresponding papers (aaai20,ijcai21).
Venus can be downloaded here.
The VeriNet toolkit is a state-of-the-art sound and complete symbolic interval propagation based toolkit for verification of neural networks. VeriNet won second place overall and was the most performing among toolkits not using GPUs in the 2nd international verification of neural networks competition. Further information can be found in the corresponding papers (ecai20,ijcai21).
VeriNet can be downloaded here.
If you cannot find the package you are looking for in any of the above pages, please do get in touch.