A Conference Management System with Verified Document Confidentiality
CAV, pp. 167-183, 2014.
We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led t...More
PPT (Upload PPT)