  This paper presents NEUROSPF, a tool for the symbolic analysis of neural
networks. Given a trained neural network model, the tool extracts the
architecture and model parameters and translates them into a Java
representation that is amenable for analysis using the Symbolic PathFinder
symbolic execution tool. Notably, NEUROSPF encodes specialized peer classes for
parsing the model's parameters, thereby enabling efficient analysis. With
NEUROSPF the user has the flexibility to specify either the inputs or the
network internal parameters as symbolic, promoting the application of program
analysis and testing approaches from software engineering to the field of
machine learning. For instance, NEUROSPF can be used for coverage-based testing
and test generation, finding adversarial examples and also constraint-based
repair of neural networks, thus improving the reliability of neural networks
and of the applications that use them. Video URL: https://youtu.be/seal8fG78LI
