Email Gateway (Aug 22 2022 at 18:54): Email Gateway (Aug 22 2022 at 18:54):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP entry.
A Formal Model of the Document Object Model
by Achim D. Brucker and Michael Herzberg
In this AFP entry, we formalize the core of the Document Object Model (DOM). At
its core, the DOM defines a tree-like data structure for representing documents
in general and HTML documents in particular. It is the heart of any modern web
browser. Formalizing the key concepts of the DOM is a prerequisite for the
formal reasoning over client-side JavaScript programs and for the analysis of
security concepts in modern web browsers. 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.
See https://www.isa-afp.org/entries/Core_DOM.html for more details.
Thanks to Achim and Michael,
René
Last updated: Apr 25 2024 at 20:15 UTC