Skip to main content
Conference Proceedings

Verifying a secure information flow analyzer

Lecture Notes in Computer Science (2005) 3603 211-226
DOI: 10.1007/11541868_14
13Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Denotational semantics for a substantial fragment of Java is formalized by deep embedding in PVS, making extensive use of dependent types. A static analyzer for secure information flow for this language is proved correct, that is, it enforces noninterference. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Naumann, D. A. (2005). Verifying a secure information flow analyzer. In Lecture Notes in Computer Science (Vol. 3603, pp. 211–226). Springer Verlag. https://doi.org/10.1007/11541868_14

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free