Compare commits
3 Commits
d44e8108aa
...
47f3f8279d
Author | SHA1 | Date |
---|---|---|
Achim D. Brucker | 47f3f8279d | |
Achim D. Brucker | 7a61fa0ba1 | |
Achim D. Brucker | 7991e67655 |
|
@ -3,7 +3,7 @@ pipeline {
|
|||
stages {
|
||||
stage('Build') {
|
||||
steps {
|
||||
sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2020 isabelle build -D /Core_SC_DOM-devel'
|
||||
sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2020 isabelle build -D /Core_SC_DOM'
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -0,0 +1,44 @@
|
|||
To cite the use of this formal theory, please use
|
||||
|
||||
|
||||
A BibTeX entry for LaTeX users is
|
||||
|
||||
|
||||
|
||||
An overview of the formalization is given in:
|
||||
|
||||
Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM
|
||||
in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
|
||||
ACM Press, 2018. doi:10.1145/3184558.3185980
|
||||
|
||||
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},
|
||||
}
|
|
@ -36,8 +36,8 @@ Assurance & Security Research Team](https://logicalhacking.com) at
|
|||
* Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM in
|
||||
Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
|
||||
ACM Press, 2018.
|
||||
https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018
|
||||
<https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018>
|
||||
* Achim D. Brucker and Michael Herzberg. Formalizing (Web) Standards: An
|
||||
Application of Test and Proof. In TAP 2018: Tests And Proofs. Lecture Notes
|
||||
in Computer Science (10889), pages 159-166, Springer-Verlag, 2018.
|
||||
https://www.brucker.ch/bibliography/abstract/brucker.ea-standard-compliance-testing-2018
|
||||
<https://www.brucker.ch/bibliography/abstract/brucker.ea-standard-compliance-testing-2018>
|
||||
|
|
Loading…
Reference in New Issue