afp-mirror
/
Core_DOM
1
0
Fork 1
Code Issues 0 Pull Requests 0 Releases 3 Wiki Activity
Local mirror of The Core DOM (Core_DOM) entry of the Archive of Formal Proofs (AFP).
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
18 Commits
1 Branch
725 KiB
 
 
 
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Core_DOM/CITATION

73 lines
4.2 KiB
Raw Permalink Blame History 

  1. To cite the use of this formal theory, please use

  2. 

  3.   Achim D. Brucker and Michael Herzberg. The Core DOM. In Archive of

  4.   Formal Proofs, 2018. http://www.isa-afp.org/entries/Core_DOM.html,

  5.   Formal proof development

  6. 

  7. A BibTeX entry for LaTeX users is

  8. 

  9. @Article{ brucker.ea:afp-core-dom:2018,

  10. 	abstract  = {In this AFP entry, we formalize the core of the Document Object Model (DOM).

  11.                      At its core, the DOM defines a tree-like data structure for representing documents

  12.                      in general and HTML documents in particular. It is the heart of any modern web

  13.                      browser. Formalizing the key concepts of the DOM is a prerequisite for the formal

  14.                      reasoning over client-side JavaScript programs and for the analysis of security

  15.                      concepts in modern web browsers. We present a formalization of the core DOM, with

  16.                      focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL.

  17.                      We use the formalization to verify the functional correctness of the most important

  18.                      functions defined in the DOM standard. Moreover, our formalization is 1) extensible,

  19.                      i.e., can be extended without the need of re-proving already proven properties

  20.                      and 2) executable, i.e., we can generate executable code from our specification.},

  21. 	author	  = {Achim D. Brucker and Michael Herzberg},

  22. 	date	  = {2018-12-26},

  23. 	file	  = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},

  24. 	filelabel = {Outline},

  25. 	issn	  = {2150-914x},

  26. 	journal	  = {Archive of Formal Proofs},

  27. 	month	  = {dec},

  28. 	note	  = {\url{http://www.isa-afp.org/entries/Core_DOM.html}, Formal proof development},

  29. 	pdf	  = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-2018.pdf},

  30. 	title	  = {The {Core} {DOM}},

  31. 	url	  = {https://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018},

  32. 	year	  = {2018},

  33. }

  34. 

  35. An overview of the formalization is given in:

  36. 

  37.   Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM 

  38.   in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749, 

  39.   ACM Press, 2018. doi:10.1145/3184558.3185980

  40. 

  41. A BibTeX entry for LaTeX users is

  42. 

  43. @InProceedings{ brucker.ea:core-dom:2018,

  44. 	abstract = {At its core, the Document Object Model (DOM) defines a tree-like           

  45.                     data structure for representing documents in general and HTML  

  46.                     documents in particular. It forms the heart of any rendering engine 

  47.                     of modern web browsers. Formalizing the key concepts of the DOM is 

  48.                     a pre-requisite for the formal reasoning over client-side JavaScript 

  49.                     programs as well as for the analysis of security concepts in modern 

  50.                     web browsers. In this paper, we present a formalization of the core DOM, 

  51.                     with focus on the node-tree and the operations defined on node-trees, 

  52.                     in Isabelle/HOL. We use the formalization to verify the functional 

  53.                     correctness of the most important functions defined in the DOM standard. 

  54.                     Moreover, our formalization is (1) extensible, i.e., can be extended without 

  55.                     the need of re-proving already proven properties and (2) executable, i.e., 

  56.                     we can generate executable code from our specification.},

  57. 	address	 = {New York, NY, USA},

  58. 	author	 = {Achim D. Brucker and Michael Herzberg},

  59. 	booktitle= {The 2018 Web Conference Companion (WWW)},

  60. 	conf_date= {April 23-27, 2018},

  61. 	doi	 = {10.1145/3184558.3185980},

  62. 	editor	 = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},

  63. 	isbn	 = {978-1-4503-5640-4/18/04},

  64. 	keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},

  65. 	location = {Lyon, France},

  66. 	pages	 = {741--749},

  67. 	pdf	 = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},

  68. 	publisher= {ACM Press},

  69. 	title	 = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},

  70. 	url	 = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},

  71. 	year	 = {2018},

  72. }