@STRING{j-fac	= "Formal Aspects of Computing" }
@STRING{pub-springer={Springer-Verlag} }
@STRING{pub-springer:adr={Heidelberg} }
@STRING{s-lncs	= "Lecture Notes in Computer Science" }

@Book{		  nipkow.ea:isabelle:2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL---A Proof Assistant for Higher-Order Logic},
  publisher	= pub-springer,
  address	= pub-springer:adr,
  series	= s-lncs,
  volume	= 2283,
  doi		= {10.1007/3-540-45949-9},
  abstract	= {This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using
		  the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for
		  researchers. The book has three parts.
		  
		  1. Elementary Techniques shows how to model functional programs in higher-order logic. Early examples
		  involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a
		  chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics
		  as nested and mutual recursion. 2. Logic and Sets presents a collection of lower-level tactics that
		  you can use to apply rules selectively. It also describes Isabelle/HOL's treatment of sets, functions
		  and relations and explains how to define sets inductively. One of the examples concerns the theory of
		  model checking, and another is drawn from a classic textbook on formal languages. 3. Advanced Material
		  describes a variety of other topics. Among these are the real numbers, records and overloading.
		  Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an
		  extended example: the verification of a security protocol. },
  year		= 2002,
  acknowledgement={brucker, 2007-02-19},
  bibkey	= {nipkow.ea:isabelle:2002}
}

@Misc{		  dom-specification,
  year		= 2016,
  month		= {DOM Living Standard -- Last Updated 20 October 2016},
  day		= 20,
  url		= {https://dom.spec.whatwg.org/},
  organization	= {Web Hypertext Application Technology Working Group (WHATWG)},
  note		= {An archived copy of the version from 20 October 2016 is available at
		  \url{https://git.logicalhacking.com/BrowserSecurity/fDOM-idl/}.}
}

@InProceedings{	  brucker.ea:core-dom:2018,
  author	= {Achim D. Brucker and Michael Herzberg},
  title		= {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
  booktitle	= {Proceedings of the Web Programming, Design, Analysis, And Implementation (WPDAI) track at WWW 2018},
  location	= {Lyon, France},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker.ea-fdom-2018},
  year		= 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. },
  keywords	= {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
  classification= {conference},
  areas		= {formal methods, software},
  public	= {yes}
}

@Article{	  klein:operating:2009,
  author	= {Gerwin Klein},
  title		= {Operating System Verification --- An Overview},
  journal	= {S\={a}dhan\={a}},
  publisher	= pub-springer,
  year		= 2009,
  volume	= 34,
  number	= 1,
  month		= feb,
  pages		= {27--69},
  abstract	= {This paper gives a high-level introduction to the topic of formal, interactive, machine-checked
		  software verification in general, and the verification of operating systems code in particular. We
		  survey the state of the art, the advantages and limitations of machine-checked code proofs, and
		  describe two specific ongoing larger-scale verification projects in more detail.}
}

@InProceedings{	  gardner.ea:securing:2009,
  author	= {Ryan W. Gardner and Sujata Garera and Matthew W. Pagano and Matthew Green and Aviel D. Rubin},
  title		= {Securing medical records on smart phones},
  booktitle	= {ACM workshop on Security and privacy in medical and home-care systems (SPIMACS)},
  year		= 2009,
  isbn		= {978-1-60558-790-5},
  pages		= {31--40},
  location	= {Chicago, Illinois, USA},
  doi		= {10.1145/1655084.1655090},
  address	= pub-acm:adr,
  publisher	= pub-acm,
  abstract	= {There is an inherent conflict between the desire to maintain privacy of one's medical records and the
		  need to make those records available during an emergency. To satisfy both objectives, we introduce a
		  flexible architecture for the secure storage of medical records on smart phones. In our system, a
		  person can view her records at any time, and emergency medical personnel can view the records as long
		  as the person is present (even if she is unconscious). Our solution allows for efficient revocation of
		  access rights and is robust against adversaries who can access the phone's storage offline.}
}

@InProceedings{	  raad.ea:dom:2016,
  author	= {Azalea Raad and Jos{\'{e}} Fragoso Santos and Philippa Gardner},
  title		= {{DOM:} Specification and Client Reasoning},
  booktitle	= {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November
		  21-23, 2016, Proceedings},
  pages		= {401--422},
  year		= 2016,
  crossref	= {igarashi:programming:2016},
  doi		= {10.1007/978-3-319-47958-3_21},
  abstract	= {We present an axiomatic specification of a key fragment of DOM using structural separation logic.
		  This specification allows us to develop modular reasoning about client programs that call the DOM.}
}

@InProceedings{	  bohannon.ea:featherweight:2010,
  author	= {Aaron Bohannon and Benjamin C. Pierce},
  title		= {Featherweight {F}irefox: {F}ormalizing the Core of a Web Browser},
  booktitle	= {Usenix Conference on Web Application Development (WebApps)},
  year		= 2010,
  month		= jun,
  url		= {http://www.cis.upenn.edu/~bohannon/browser-model/},
  abstract	= {We offer a formal specification of the core functionality of a web browser in the form of a
		  small-step operational semantics. The specification accurately models the asyn- chronous nature of web
		  browsers and covers the basic as- pects of windows, DOM trees, cookies, HTTP requests and responses,
		  user input, and a minimal scripting lan- guage with first-class functions, dynamic evaluation, and
		  AJAX requests. No security enforcement mechanisms are included{\^a}instead, the model is intended to
		  serve as a basis for formalizing and experimenting with different security policies and mechanisms. We
		  survey the most interesting design choices and discuss how our model re- lates to real web browsers.}
}

@Proceedings{	  joyce.ea:higher:1994,
  editor	= {Jeffrey J. Joyce and Carl-Johan H. Seger},
  title		= {Higher Order Logic Theorem Proving and Its Applications (HUG)},
  booktitle	= {Higher Order Logic Theorem Proving and Its Applications (HUG)},
  publisher	= pub-springer,
  address	= pub-springer:adr,
  series	= s-lncs,
  abstract	= {Theorem proving based techniques for formal hardware verification have been evolving constantly and
		  researchers are getting able to reason about more complex issues than it was possible or practically
		  feasible in the past. It is often the case that a model of a system is built in a formal logic and
		  then reasoning about this model is carried out in the logic. Concern is growing on how to consistently
		  interface a model built in a formal logic with an informal CAD environment. Researchers have been
		  investigating how to define the formal semantics of hardware description languages so that one can
		  formally reason about models informally dealt with in a CAD environment. At the University of
		  Cambridge, the embedding of hardware description languages in a logic is classified in two categories:
		  deep embedding and shallow embedding. In this paper we argue that there are degrees of formality in
		  shallow embedding a language in a logic. The choice of the degree of formality is a trade-off between
		  the security of the embedding and the amount and complexity of the proof effort in the logic. We also
		  argue that the design of a language could consider this verifiability issue. There are choices in the
		  design of a language that can make it easier to improve the degree of formality, without implying
		  serious drawbacks for the CAD environment.},
  volume	= 780,
  year		= 1994,
  doi		= {10.1007/3-540-57826-9},
  isbn		= {3-540-57826-9},
  acknowledgement={brucker, 2007-02-19}
}

@Misc{		  whatwg:dom:2017,
  key		= {whatwg},
  author	= {{WHATWG}},
  url		= {https://dom.spec.whatwg.org/commit-snapshots/6253e53af2fbfaa6d25ad09fd54280d8083b2a97/},
  month		= mar,
  year		= 2017,
  day		= 24,
  title		= {{DOM} -- Living Standard},
  note		= {Last Updated 24 {March} 2017},
  institution	= {WHATWG}
}

@Misc{		  whatwg:html:2017,
  key		= {whatwg},
  author	= {{WHATWG}},
  url		= {https://html.spec.whatwg.org/},
  month		= apr,
  year		= 2017,
  day		= 13,
  title		= {{HTML} -- Living Standard},
  note		= {Last Updated 13 {April} 2017},
  institution	= {WHATWG}
}

@Misc{		  w3c:dom:2015,
  key		= {w3c},
  author	= {{W3C}},
  url		= {https://www.w3.org/TR/dom/},
  month		= nov,
  year		= 2015,
  day		= 19,
  title		= {{W3C} {DOM4}},
  institution	= {W3C}
}

@Proceedings{	  igarashi:programming:2016,
  editor	= {Atsushi Igarashi},
  title		= {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November
		  21-23, 2016, Proceedings},
  series	= {Lecture Notes in Computer Science},
  volume	= 10017,
  year		= 2016,
  doi		= {10.1007/978-3-319-47958-3},
  isbn		= {978-3-319-47957-6}
}

@InProceedings{	  gardner.ea:dom:2008,
  author	= {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
  title		= {{DOM:} Towards a Formal Specification},
  booktitle	= {{PLAN-X} 2008, Programming Language Technologies for XML, An {ACM} {SIGPLAN} Workshop colocated with
		  {POPL} 2008, San Francisco, California, USA, January 9, 2008},
  year		= 2008,
  crossref	= {plan-x:2008},
  url		= {http://gemo.futurs.inria.fr/events/PLANX2008/papers/p18.pdf},
  abstract	= {The W3C Document Object Model (DOM) specifies an XML up- date library. DOM is written in English, and
		  is therefore not compo- sitional and not complete. We provide a first step towards a compo- sitional
		  specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a
		  complete reason- ing for straight-line code. Our work transfers O{\^a}Hearn, Reynolds and Yang{\^a}s
		  local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM.
		  In par- ticular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about
		  a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only
		  formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g.
		  invariant properties of simple Javascript programs.}
}

@InProceedings{	  jang.ea:establishing:2012,
  author	= {Dongseok Jang and Zachary Tatlock and Sorin Lerner},
  title		= {Establishing Browser Security Guarantees through Formal Shim Verification},
  booktitle	= {Proceedings of the 21th {USENIX} Security Symposium, Bellevue, WA, USA, August 8-10, 2012},
  pages		= {113--128},
  year		= 2012,
  crossref	= {kohno:proceedings:2012},
  url		= {https://www.usenix.org/conference/usenixsecurity12/technical-sessions/presentation/jang},
  abstract	= { Web browsers mediate access to valuable private data in domains ranging from health care to banking.
		  Despite this critical role, attackers routinely exploit browser vulnerabilities to exfiltrate private
		  data and take over the un- derlying system. We present Q UARK , a browser whose kernel has been
		  implemented and verified in Coq. We give a specification of our kernel, show that the implementation
		  satisfies the specification, and finally show that the specification implies several security
		  properties, including tab non-interference, cookie integrity and confidentiality, and address bar
		  integrity. }
}

@Proceedings{	  kohno:proceedings:2012,
  editor	= {Tadayoshi Kohno},
  title		= {Proceedings of the 21th {USENIX} Security Symposium, Bellevue, WA, USA, August 8-10, 2012},
  publisher	= {{USENIX} Association},
  year		= 2012,
  timestamp	= {Thu, 15 May 2014 09:12:27 +0200}
}

@Proceedings{	  plan-x:2008,
  title		= {{PLAN-X} 2008, Programming Language Technologies for XML, An {ACM} {SIGPLAN} Workshop colocated with
		  {POPL} 2008, San Francisco, California, USA, January 9, 2008},
  year		= 2008,
  timestamp	= {Fri, 18 Jan 2008 13:01:04 +0100}
}

@Article{	  brucker.ea:extensible:2008-b,
  abstract	= {We present an extensible encoding of object-oriented data models into HOL. Our encoding is supported
		  by a datatype package that leverages the use of the shallow embedding technique to object-oriented
		  specification and programming languages. The package incrementally compiles an object-oriented data
		  model, i.e., a class model, to a theory containing object-universes, constructors, accessor functions,
		  coercions (casts) between dynamic and static types, characteristic sets, and co-inductive class
		  invariants. The package is conservative, i.e., all properties are derived entirely from constant
		  definitions, including the constraints over object structures. As an application, we use the package
		  for an object-oriented core-language called IMP++, for which we formally prove the correctness of a
		  Hoare-Logic with respect to a denotational semantics.},
  address	= {Heidelberg},
  author	= {Achim D. Brucker and Burkhart Wolff},
  doi		= {10.1007/s10817-008-9108-3},
  issn		= {0168-7433},
  issue		= 3,
  journal	= {Journal of Automated Reasoning},
  keywords	= {object-oriented data models, HOL, theorem proving, verification},
  language	= {USenglish},
  pages		= {219--249},
  pdf		= {https://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf},
  publisher	= {Springer-Verlag},
  title		= {An Extensible Encoding of Object-oriented Data Models in HOL},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b},
  volume	= 41,
  year		= 2008
}

@PhDThesis{	  brucker:interactive:2007,
  abstract	= {We present a semantic framework for object-oriented specification languages. We develop this
		  framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions
		  guarantees by construction the consistency of our formalization. Moreover, we show how our framework
		  can be used to build an interactive proof environment, called HOL-OCL, for object-oriented
		  specifications in general and for UML/OCL in particular.\\\\Our main contributions are an extensible
		  encoding of object-oriented data structures in HOL, a datatype package for object-oriented
		  specifications, and the development of several equational and tableaux calculi for object-oriented
		  specifications. Further, we show that our formal framework can be the basis of a formal
		  machine-checked semantics for OCL that is compliant to the OCL 2.0 standard.},
  abstract_de	= {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r objektorientierte Spezifikationen
		  vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch
		  die Beschr{\"a}nkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung
		  garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL
		  f{\"u}r objektorientierte Spezifikationen im Allgemeinen und insbesondere f{\"u}r UML/OCL zu
		  entwickeln.\\\\Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung
		  objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r objektorientierte
		  Spezifikationen und die Entwicklung verschiedener Kalk{\"u}le f{\"u}r objektorientierte
		  Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale,
		  maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die konform zum Standard f{\"u}r OCL 2.0 ist.},
  author	= {Achim D. Brucker},
  keywords	= {OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL},
  month		= {mar},
  note		= {ETH Dissertation No. 17097.},
  pdf		= {https://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf},
  school	= {ETH Zurich},
  title		= {An Interactive Proof Environment for Object-oriented Specifications},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker-interactive-2007},
  year		= 2007
}

@InCollection{	  brucker.ea:standard-compliance-testing:2018,
  talk		= {talk:brucker.ea:standard-compliance-testing:2018},
  abstract	= {Most popular technologies are based on informal or semiformal standards that lack a rigid formal
		  semantics. Typical examples include web technologies such as the DOM or HTML, which are defined by the
		  Web Hypertext Application Technology Working Group (WHATWG) and the World Wide Web Consortium (W3C).
		  While there might be API specifications and test cases meant to assert the compliance of a certain
		  implementation, the actual standard is rarely accompanied by a formal model that would lend itself
		  for, e.g., verifying the security or safety properties of real systems.
		  
		  Even when such a formalization of a standard exists, two important questions arise: first, to what
		  extend does the formal model comply to the standard and, second, to what extend does the
		  implementation comply to the formal model and the assumptions made during the verification? In this
		  paper, we present an approach that brings all three involved artifacts - the (semi-)formal standard,
		  the formalization of the standard, and the implementations - closer together by combining
		  verification, symbolic execution, and specification based testing.},
  keywords	= {standard compliance, compliance tests, DOM},
  location	= {Toulouse, France},
  author	= {Achim D. Brucker and Michael Herzberg},
  booktitle	= {{TAP} 2018: Tests And Proofs},
  language	= {USenglish},
  publisher	= pub-springer,
  address	= pub-springer:adr,
  series	= s-lncs,
  number	= 10889,
  editor	= {Cathrine Dubois and Burkhart Wolff},
  title		= {Formalizing (Web) Standards: An Application of Test and Proof},
  categories	= {holtestgen, websecurity},
  classification= {conference},
  areas		= {formal methods, software engineering},
  public	= {yes},
  year		= 2018,
  doi		= {10.1007/978-3-319-92994-1_9},
  pages		= {159--166},
  isbn		= {978-3-642-38915-3},
  pdf		= {http://www.brucker.ch/bibliography/download/2018/brucker.ea-standard-compliance-testing-2018.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-standard-compliance-testing-2018}
}

@InCollection{	  brucker.ea:interactive:2005,
  keywords	= {symbolic test case generations, black box testing, white box testing, theorem proving, interactive
		  testing},
  abstract	= {HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant
		  Isabelle/HOL\@. While there is considerable skepticism with regard to interactive theorem provers in
		  testing communities, we argue that they are a natural choice for (automated) symbolic computations
		  underlying systematic tests. This holds in particular for the development on non-trivial formal test
		  plans of complex software, where some parts of the overall activity require inherently guidance by a
		  test engineer. In this paper, we present the underlying methods for both black box and white box
		  testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical
		  and conceptual framework for presenting and investigating the variety of unit test techniques in a
		  logically consistent way. },
  location	= {Edinburgh},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {Formal Approaches to Testing of Software},
  language	= {USenglish},
  publisher	= pub-springer,
  address	= pub-springer:adr,
  series	= s-lncs,
  number	= 3997,
  doi		= {10.1007/11759744_7},
  isbn		= {3-540-25109-X},
  editor	= {Wolfgang Grieskamp and Carsten Weise},
  pdf		= {http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf},
  project	= {CSFMDOS},
  title		= {Interactive Testing using {HOL}-{TestGen}},
  classification= {workshop},
  areas		= {formal methods, software},
  categories	= {holtestgen},
  year		= 2005,
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005}
}

@Article{	  brucker.ea:theorem-prover:2012,
  author	= {Achim D. Brucker and Burkhart Wolff},
  journal	= j-fac,
  publisher	= pub-springer,
  address	= pub-springer:adr,
  language	= {USenglish},
  categories	= {holtestgen},
  title		= {On Theorem Prover-based Testing},
  year		= 2013,
  issn		= {0934-5043},
  pages		= {683--721},
  volume	= 25,
  number	= 5,
  classification= {journal},
  areas		= {formal methods, software},
  public	= {yes},
  doi		= {10.1007/s00165-012-0222-y},
  keywords	= {test case generation, domain partitioning, test sequence, theorem proving, HOL-TestGen},
  abstract	= {HOL-TestGen is a specification and test case generation environment extending the interactive theorem
		  prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive
		  theorem proving, test case generation, and test data generation.
		  
		  The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by
		  transformation into a normal form called test theorem. Second, the test cases are analyzed for ground
		  instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on
		  the control of explicit test-hypotheses which can be proven over concrete programs.
		  
		  Due to the generality of the underlying framework, our system can be used for black-box unit,
		  sequence, reactive sequence and white-box test scenarios. Although based on particularly clean
		  theoretical foundations, the system can be applied for substantial case-studies. },
  pdf		= {http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012}
}

@Article{	  brucker.ea:afp-core-dom:2018,
  abstract	= {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.},
  author	= {Achim D. Brucker and Michael Herzberg},
  date		= {2018-12-26},
  file		= {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},
  filelabel	= {Outline},
  issn		= {2150-914x},
  journal	= {Archive of Formal Proofs},
  month		= {dec},
  note		= {\url{http://www.isa-afp.org/entries/Core_DOM.html}, Formal proof development},
  pdf		= {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-2018.pdf},
  title		= {The Core {DOM}},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018-a},
  year		= 2018
}

@InCollection{	  brucker.ea:web-components:2019,
  abstract	= {The trend towards ever more complex client-side web applications is unstoppable. Compared to
		  traditional software development, client-side web development lacks a well-established component
		  model, i.e., a method for easily and safely reusing already developed functionality. To address this
		  issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM):
		  shadow trees allow developers to "partition" a DOM instance into parts that should be safely
		  separated, e.g., code modifying one part should not, unintentionally, affect other parts of the
		  DOM.\\\\While 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 this paper, 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.},
  address	= {Heidelberg},
  author	= {Achim D. Brucker and Michael Herzberg},
  booktitle	= {Formal Aspects of Component Software (FACS)},
  doi		= {10.1007/978-3-030-40914-2_3},
  editor	= {Sung-Shik Jongmans and Farhad Arbab},
  isbn		= {3-540-25109-X},
  keywords	= {Web Component, Shadow Tree, DOM, Isabelle/HOL},
  language	= {USenglish},
  location	= {Amsterdam, The Netherlands},
  number	= 12018,
  pdf		= {https://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  title		= {A Formally Verified Model of Web Components},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019},
  year		= 2020
}

@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		= {download/2020/brucker.ea-afp-dom-components-2020.pdf},
  filelabel	= {Outline},
  file		= {download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
  areas		= {formal methods, security, software engineering}
}

@Article{	  brucker.ea:afp-dom-components:2020-a,
  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		= {download/2020/brucker.ea-afp-dom-components-2020.pdf},
  filelabel	= {Outline},
  file		= {download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
  areas		= {formal methods, security, software engineering}
}

@Article{         brucker.ea:afp-core-sc-dom:2020,
  author        = {Achim D. Brucker and Michael Herzberg},
  title         = {The Safely Composable {DOM}},
  journal       = {Archive of Formal Proofs},
  month         = sep,
  year          = 2020,
  date          = {2020-09-28},
  note          = {\url{http://www.isa-afp.org/entries/Core_SC_DOM.html}, Formal proof development},
  issn          = {2150-914x},
  abstract      = { In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM).
                  The SC DOM improve the standard DOM by strengthening the tree boundaries set by shadow roots: in the
                  SC DOM, the shadow root is a sub-class of the document class (instead of a base class).

                  This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the
                  nearest shadow root rather than the document root. As a result, many API methods that, when called on
                  a node inside a shadow tree, would previously ``break out'' and return or modify nodes that are
                  possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes
                  programs that operate on shadow trees more predictable for the developer and allows them to make more
                  assumptions about other code accessing the DOM. },
  public        = {yes},
  classification= {formal},
  categories    = {websecurity},
  pdf           = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-2018.pdf},
  filelabel     = {Outline},
  file          = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-outline-2018.pdf},
  areas         = {formal methods, security, software engineering},
  url           = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-sc-dom-2020}
}


@Article{         brucker.ea:afp-shadow-dom:2020,
  author        = {Achim D. Brucker and Michael Herzberg},
  title         = {Shadow DOM: A Formal Model of the Document Object Model \emph{with Shadow Roots}},
  journal       = {Archive of Formal Proofs},
  month         = sep,
  year          = 2020,
  date          = {2020-09-28},
  note          = {\url{http://www.isa-afp.org/entries/Shadow_DOM.html}, Formal proof development},
  issn          = {2150-914x},
  abstract      = { In this AFP entry, we extend our formalization of the core DOM with \emph{Shadow Roots}. Shadow
                  roots are a recent proposal of the web community to support a component-based development approach for
                  client-side web applications.

                  Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be
                  backward compatible, such extensions often result in complex specification that may contain unwanted
                  subtleties that can be detected by a formalization.

                  Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our
                  formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can
                  be extended without the need of re-proving already proven properties and executable, i.e., we can
                  generate executable code from our specification. We exploit the executability to show that our
                  formalization complies to the official standard of the W3C, respectively, the WHATWG. },
  public        = {yes},
  classification= {formal},
  categories    = {websecurity},
  pdf           = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-dom-2018.pdf},
  filelabel     = {Outline},
  file          = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-dom-outline-2018.pdf},
  areas         = {formal methods, security, software engineering},
  url           = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-shadow-dom-2020}
}
                                                                          
@Article{         brucker.ea:afp-sc-dom-components:2020,
  author        = {Achim D. Brucker and Michael Herzberg},
  title         = {A Formalization of Safely Composable Web Components},
  journal       = {Archive of Formal Proofs},
  month         = sep,
  year          = 2020,
  date          = {2020-09-28},
  note          = {\url{http://www.isa-afp.org/entries/SC_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-sc-dom-components-2020.pdf},
  filelabel     = {Outline},
  file          = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-sc-dom-components-outline-2020.pdf},
  areas         = {formal methods, security, software engineering},
  url           = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-sc-dom-components-2020}
}
   

@PhdThesis{herzberg:web-components:2020,
  author =       {Michael Herzberg},
  title =        {Formal Foundations for Provably Safe Web Components},
  school =       {The University of Sheffield},
  year =         {2020}
}

