Name
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11541868_14 | TPHOLs |
Keywords | Field | DocType |
secure information flow,extensive use,denotational semantics,secure information flow analyzer,substantial fragment,static analyzer,deep embedding,dependent type,dependent types | Programming language,Embedding,Semantic domain,Computer science,Denotational semantics,Automated theorem proving,Static analysis,Proof theory,Algorithm,Theoretical computer science,Java,Proof assistant | Conference |
Volume | ISSN | ISBN |
3603 | 0302-9743 | 3-540-28372-2 |
Citations | PageRank | References |
10 | 0.68 | 13 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| David Naumann | 1 | 1101 | 84.12 |