BibTex format
@phdthesis{Wood:2013,
author = {Wood, T},
title = {A Program Logic for Verification of Security Properties of Secure ECMAScript Programs},
url = {http://www.doc.ic.ac.uk/~tw1509/},
year = {2013}
}
Publications
Citation
RIS format (EndNote, RefMan)
TY - THES
AB - We present an Operational Semantics of the Secure ECMAScript (SES) language. We extend Separation Logic with a backpointer operator to permit reasoning about reachability in the object graph whilst maintaining local reasoning. We define inference rules in the extended logic for SES. Finally, we prove the correctness of the Membrane design pattern.
AU - Wood,T
PY - 2013///
TI - A Program Logic for Verification of Security Properties of Secure ECMAScript Programs
UR - http://www.doc.ic.ac.uk/~tw1509/
ER -