Browse Source

Fixed BibTeX entry.

main afp-current-Isabelle2021
Achim D. Brucker 8 months ago
parent
commit
1d11150cfa
  1. 59
      CITATION

59
CITATION

@ -7,36 +7,35 @@ To cite the use of this formal theory, please use
A BibTeX entry for LaTeX users is
@InProceedings{ brucker.ea:core-dom:2018,
abstract = {At its core, the Document Object Model (DOM) defines a tree-like
data structure for representing documents in general and HTML
documents in particular. It forms the heart of any rendering engine
of modern web browsers. Formalizing the key concepts of the DOM is
a pre-requisite for the formal reasoning over client-side JavaScript
programs as well as for the analysis of security concepts in modern
web browsers. In this paper, we present a formalization of the core DOM,
with focus on the node-tree and the operations defined on node-trees,
in Isabelle/HOL. We use the formalization to verify the functional
correctness of the most important functions defined in the DOM standard.
Moreover, our formalization is (1) extensible, i.e., can be extended without
the need of re-proving already proven properties and (2) executable, i.e.,
we can generate executable code from our specification.},
address = {New York, NY, USA},
author = {Achim D. Brucker and Michael Herzberg},
booktitle= {The 2018 Web Conference Companion (WWW)},
conf_date= {April 23-27, 2018},
doi = {10.1145/3184558.3185980},
editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},
isbn = {978-1-4503-5640-4/18/04},
keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
location = {Lyon, France},
pages = {741--749},
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},
publisher= {ACM Press},
title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},
year = {2018},
}
@Article{ brucker.ea:afp-dom-components:2020,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formalization of Web Components},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
date = {2020-09-28},
note = {\url{http://www.isa-afp.org/entries/DOM_Components.html}, Formal proof development},
issn = {2150-914x},
public = {yes},
classification= {formal},
categories = {websecurity},
pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-2020.pdf},
filelabel = {Outline},
file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
areas = {formal methods, security, software engineering},
abstract = { While the DOM with shadow trees provide the technical basis for defining web components, the DOM
standard neither defines the concept of web components nor specifies the safety properties that web
components should guarantee. Consequently, the standard also does not discuss how or even if the
methods for modifying the DOM respect component boundaries.
In AFP entry, we present a formally verified model of web components and define safety properties
which ensure that different web components can only interact with each other using well-defined
interfaces. Moreover, our verification of the application programming interface (API) of the DOM
revealed numerous invariants that implementations of the DOM API need to preserve to ensure the
integrity of components. },
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-dom-components-2020}
}
An overview of the formalization is given in:

Loading…
Cancel
Save