This verification example covers a common security property: a secure device does not send out data when it received privacy-sensitive information. Model-based abstraction is used to verify that the program adheres to a process algebra abstraction, which does not perform a 'send' action after receiving privacy-sensitive information.
Path to example file
Lines of code
127 lines (comments not included)
Lines of specification
66 lines (51.97% of the total)
Note, verification may take a while and has a time-out of 20 seconds.