Applications of Interactive Proof to Data Flow Analysis and Security
Klein Gerwin, Nipkow Tobias · NATO science for peace and security series. D, Information and communication security · 2014
We show how to formalise a small imperative programming language in the theorem prover Isabelle/HOL, how to define its semantics, and how to prove properties about the language, its type systems, and a number of data flow analyses.