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.

General Information

  • Backend: Silicon
  • Language: Java
  • Features: Futures
  • Path to Example File: futures/
  • Should Verify: Yes
  • Date: 2017-06-16
  • Lines of Code: 127 (comments not included)
  • Lines of Specification: 66 (52.0% of total)
  • Computation Time: 25.3 seconds