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.
 
 
 

73 lines
4.2 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker and Michael Herzberg. The Core DOM. In Archive of
  3. Formal Proofs, 2018. http://www.isa-afp.org/entries/Core_DOM.html,
  4. Formal proof development
  5. A BibTeX entry for LaTeX users is
  6. @Article{ brucker.ea:afp-core-dom:2018,
  7. abstract = {In this AFP entry, we formalize the core of the Document Object Model (DOM).
  8. At its core, the DOM defines a tree-like data structure for representing documents
  9. in general and HTML documents in particular. It is the heart of any modern web
  10. browser. Formalizing the key concepts of the DOM is a prerequisite for the formal
  11. reasoning over client-side JavaScript programs and for the analysis of security
  12. concepts in modern web browsers. We present a formalization of the core DOM, with
  13. focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL.
  14. We use the formalization to verify the functional correctness of the most important
  15. functions defined in the DOM standard. Moreover, our formalization is 1) extensible,
  16. i.e., can be extended without the need of re-proving already proven properties
  17. and 2) executable, i.e., we can generate executable code from our specification.},
  18. author = {Achim D. Brucker and Michael Herzberg},
  19. date = {2018-12-26},
  20. file = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},
  21. filelabel = {Outline},
  22. issn = {2150-914x},
  23. journal = {Archive of Formal Proofs},
  24. month = {dec},
  25. note = {\url{http://www.isa-afp.org/entries/Core_DOM.html}, Formal proof development},
  26. pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-2018.pdf},
  27. title = {The {Core} {DOM}},
  28. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018},
  29. year = {2018},
  30. }
  31. An overview of the formalization is given in:
  32. Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM
  33. in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
  34. ACM Press, 2018. doi:10.1145/3184558.3185980
  35. A BibTeX entry for LaTeX users is
  36. @InProceedings{ brucker.ea:core-dom:2018,
  37. abstract = {At its core, the Document Object Model (DOM) defines a tree-like
  38. data structure for representing documents in general and HTML
  39. documents in particular. It forms the heart of any rendering engine
  40. of modern web browsers. Formalizing the key concepts of the DOM is
  41. a pre-requisite for the formal reasoning over client-side JavaScript
  42. programs as well as for the analysis of security concepts in modern
  43. web browsers. In this paper, we present a formalization of the core DOM,
  44. with focus on the node-tree and the operations defined on node-trees,
  45. in Isabelle/HOL. We use the formalization to verify the functional
  46. correctness of the most important functions defined in the DOM standard.
  47. Moreover, our formalization is (1) extensible, i.e., can be extended without
  48. the need of re-proving already proven properties and (2) executable, i.e.,
  49. we can generate executable code from our specification.},
  50. address = {New York, NY, USA},
  51. author = {Achim D. Brucker and Michael Herzberg},
  52. booktitle= {The 2018 Web Conference Companion (WWW)},
  53. conf_date= {April 23-27, 2018},
  54. doi = {10.1145/3184558.3185980},
  55. editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},
  56. isbn = {978-1-4503-5640-4/18/04},
  57. keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
  58. location = {Lyon, France},
  59. pages = {741--749},
  60. pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},
  61. publisher= {ACM Press},
  62. title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
  63. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},
  64. year = {2018},
  65. }