Different methods to verify a neural network controller encoded on a PLC program are presented in these files. Each of the main folders contains a different approach.

PLCverif_CBMC/PLCverifProject contains the original PLC code. PLCverif_CBMC has the C code that is executed by CBMC to verify all the properties. nnenum contains the code used to verify different properties using the neural network verifier nnenum. testing has the Jupyter notebook that was used to test all the combinations of the inputs and check if the properties were satisfied. Z3 holds the Jupyter notebook that uses the Python API of Z3 to verify different properties. The README file contains some instructions to run the different files.