Verification of a neural network controller encoded on a PLC program

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.