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.
Original language | English |
---|---|
Pages (from-to) | 211-226 |
Number of pages | 16 |
Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Volume | 3603 |
DOIs | |
State | Published - 2005 |
Event | 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 - Oxford, United Kingdom Duration: 22 Aug 2005 → 25 Aug 2005 |