
@Article{	  noschinski:graph:2013,
  author	= {Lars Noschinski},
  title		= {{Graph} {Theory}},
  journal	= {Archive of Formal Proofs},
  month		= apr,
  year		= 2013,
  note		= {\url{https://isa-afp.org/entries/Graph_Theory.html}, Formal proof development},
  issn		= {2150-914x}
}

@Article{	  eberl:erf:2018,
  author	= {Manuel Eberl},
  title		= {The {Error} {Function}},
  journal	= {Archive of Formal Proofs},
  month		= feb,
  year		= 2018,
  note		= {\url{https://isa-afp.org/entries/Error_Function.html}, Formal proof development},
  issn		= {2150-914x}
}

@Book{		  aggarwal:neural:2018,
  author	= {Charu C. Aggarwal},
  title		= {Neural Networks and Deep Learning: A Textbook},
  year		= 2018,
  isbn		= 3319944622,
  publisher	= {Springer Publishing Company, Incorporated},
  edition	= {1st},
  abstract	= {This book covers both classical and modern models in deep learning. The primary focus is on the
		  theory and algorithms of deep learning. The theory and algorithms of neural networks are particularly
		  important for understanding important concepts, so that one can understand the important design
		  concepts of neural architectures in different applications. Why do neural networks work? When do they
		  work better than off-the-shelf machine-learning models? When is depth useful? Why is training neural
		  networks so hard? What are the pitfalls? The book is also rich in discussing different applications in
		  order to give the practitioner a flavor of how neural architectures are designed for different types
		  of problems. Applications associated with many different areas like recommender systems, machine
		  translation, image captioning, image classification, reinforcement-learning based gaming, and text
		  analytics are covered. The chapters of this book span three categories: The basics of neural networks:
		  Many traditional machine learning models can be understood as special cases of neural networks. An
		  emphasis is placed in the first two chapters on understanding the relationship between traditional
		  machine learning and neural networks. Support vector machines, linear/logistic regression, singular
		  value decomposition, matrix factorization, and recommender systems are shown to be special cases of
		  neural networks. These methods are studied together with recent feature engineering methods like
		  word2vec. Fundamentals of neural networks: A detailed discussion of training and regularization is
		  provided in Chapters 3 and 4. Chapters 5 and 6 present radial-basis function (RBF) networks and
		  restricted Boltzmann machines. Advanced topics in neural networks: Chapters 7 and 8 discuss recurrent
		  neural networks and convolutional neural networks. Several advanced topics like deep reinforcement
		  learning, neural Turing machines, Kohonen self-organizing maps, and generative adversarial networks
		  are introduced in Chapters 9 and 10. The book is written for graduate students, researchers, and
		  practitioners. Numerous exercises are available along with a solution manual to aid in classroom
		  teaching. Where possible, an application-centric view is highlighted in order to provide an
		  understanding of the practical uses of each class of techniques.}
}

@Book{		  skansi:introduction:2018,
  author	= {Sandro Skansi},
  title		= {Introduction to Deep Learning: From Logical Calculus to Artificial Intelligence},
  year		= 2018,
  isbn		= 3319730037,
  publisher	= {Springer Publishing Company, Incorporated},
  edition	= {1st},
  abstract	= {This textbook presents a concise, accessible and engaging first introduction to deep learning,
		  offering a wide range of connectionist models which represent the current state-of-the-art. The text
		  explores the most popular algorithms and architectures in a simple and intuitive style, explaining the
		  mathematical derivations in a step-by-step manner. The content coverage includes convolutional
		  networks, LSTMs, Word2vec, RBMs, DBNs, neural Turing machines, memory networks and autoencoders.
		  Numerous examples in working Python code are provided throughout the book, and the code is also
		  supplied separately at an accompanying website. Topics and features: introduces the fundamentals of
		  machine learning, and the mathematical and computational prerequisites for deep learning; discusses
		  feed-forward neural networks, and explores the modifications to these which can be applied to any
		  neural network; examines convolutional neural networks, and the recurrent connections to a
		  feed-forward neural network; describes the notion of distributed representations, the concept of the
		  autoencoder, and the ideas behind language processing with deep learning; presents a brief history of
		  artificial intelligence and neural networks, and reviews interesting open research problems in deep
		  learning and connectionism. This clearly written and lively primer on deep learning is essential
		  reading for graduate and advanced undergraduate students of computer science, cognitive science and
		  mathematics, as well as fields such as linguistics, logic, philosophy, and psychology.}
}

@Book{		  russell.ea:artificial:2009,
  author	= {Stuart Russell and Peter Norvig},
  title		= {Artificial Intelligence: A Modern Approach},
  year		= 2009,
  isbn		= 0136042597,
  publisher	= {Prentice Hall Press},
  address	= {USA},
  edition	= {3rd},
  abstract	= { The long-anticipated revision of this #1 selling book offers the most comprehensive, state of the
		  art introduction to the theory and practice of artificial intelligence for modern applications.
		  Intelligent Agents. Solving Problems by Searching. Informed Search Methods. Game Playing. Agents that
		  Reason Logically. First-order Logic. Building a Knowledge Base. Inference in First-Order Logic.
		  Logical Reasoning Systems. Practical Planning. Planning and Acting. Uncertainty. Probabilistic
		  Reasoning Systems. Making Simple Decisions. Making Complex Decisions. Learning from Observations.
		  Learning with Neural Networks. Reinforcement Learning. Knowledge in Learning. Agents that Communicate.
		  Practical Communication in English. Perception. Robotics. For computer professionals, linguists, and
		  cognitive scientists interested in artificial intelligence. }
}

@Misc{		  dua.ea:uci:2017,
  author	= {Dua, Dheeru and Graff, Casey},
  year		= 2017,
  title		= {{UCI} Machine Learning Repository},
  url		= {http://archive.ics.uci.edu/ml},
  institution	= {University of California, Irvine, School of Information and Computer Sciences}
}

@Misc{		  abadi.ea:tensorflow:2015,
  title		= {{TensorFlow}: Large-Scale Machine Learning on Heterogeneous Systems},
  url		= {https://www.tensorflow.org/},
  note		= {Software available from tensorflow.org},
  author	= {Mart\'{i}n Abadi and Ashish Agarwal and Paul Barham and Eugene Brevdo and Zhifeng Chen and Craig
		  Citro and Greg S.~Corrado and Andy Davis and Jeffrey Dean and Matthieu Devin and Sanjay Ghemawat and
		  Ian Goodfellow and Andrew Harp and Geoffrey Irving and Michael Isard and Yangqing Jia and Rafal
		  Jozefowicz and Lukasz Kaiser and Manjunath Kudlur and Josh Levenberg and Dandelion Man\'{e} and Rajat
		  Monga and Sherry Moore and Derek Murray and Chris Olah and Mike Schuster and Jonathon Shlens and
		  Benoit Steiner and Ilya Sutskever and Kunal Talwar and Paul Tucker and Vincent Vanhoucke and Vijay
		  Vasudevan and Fernanda Vi\'{e}gas and Oriol Vinyals and Pete Warden and Martin Wattenberg and Martin
		  Wicke and Yuan Yu and Xiaoqiang Zheng},
  year		= 2015
}

@Article{	  fisher:use:1936,
  author	= {R.A. Fisher},
  title		= {The Use of Multiple Measurements in Taxonomic Problems},
  journal	= {Annals of Eugenics},
  volume	= 7,
  number	= 2,
  pages		= {179--188},
  doi		= {10.1111/j.1469-1809.1936.tb02137.x},
  abstract	= {The articles published by the Annals of Eugenics (1925--1954) have been made available online as an
		  historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice
		  against racial, ethnic and disabled groups. The online publication of this material for scholarly
		  research purposes is not an endorsement of those views nor a promotion of eugenics in any way.},
  year		= 1936
}

@Article{	  smilkov.ea:tensorflowjs:2019,
  author	= {Daniel Smilkov and Nikhil Thorat and Yannick Assogba and Ann Yuan and Nick Kreeger and Ping Yu and
		  Kangyi Zhang and Shanqing Cai and Eric Nielsen and David Soergel and Stan Bileschi and Michael Terry
		  and Charles Nicholson and Sandeep N. Gupta and Sarah Sirajuddin and D. Sculley and Rajat Monga and
		  Greg Corrado and Fernanda B. Vi{\'{e}}gas and Martin Wattenberg},
  title		= {TensorFlow.js: Machine Learning for the Web and Beyond},
  journal	= {CoRR},
  volume	= {abs/1901.05350},
  year		= 2019,
  url		= {http://arxiv.org/abs/1901.05350},
  eprinttype	= {arXiv},
  eprint	= {1901.05350}
}

@Booklet{	  ecma:json:2017,
  title		= {{ECMA-404}:The {JSON} data interchange syntax},
  howpublished	= {Online: \url{https://www.ecma-international.org/publications-and-standards/standards/ecma-404/}.},
  edition	= {2nd},
  month		= dec,
  year		= 2017
}

@Misc{		  ietf:rfc8259-json:2017,
  issn		= {2070-1721},
  title		= {The {JavaScript} {Object} {Notation} ({JSON}) {Data} {Interchange} {Format}},
  howpublished	= {Online: \url{https://datatracker.ietf.org/doc/html/rfc8259}.},
  month		= dec,
  year		= 2017,
  editor	= {T. Bray}
}

@Article{	  brucker:nano-json:2022,
  author	= {Achim D. Brucker},
  title		= {{Nano} {JSON}},
  journal	= {Archive of Formal Proofs},
  year		= 2022,
  note		= {\url{https://isa-afp.org/entries/Nano_JSON.html}, Formal proof development},
  issn		= {2150-914x}
}

@Article{	  harris.ea:array:2020,
  title		= {Array programming with {NumPy}},
  author	= {Charles R. Harris and K. Jarrod Millman and St{\'{e}}fan J. van der Walt and Ralf Gommers and Pauli
		  Virtanen and David Cournapeau and Eric Wieser and Julian Taylor and Sebastian Berg and Nathaniel J.
		  Smith and Robert Kern and Matti Picus and Stephan Hoyer and Marten H. van Kerkwijk and Matthew Brett
		  and Allan Haldane and Jaime Fern{\'{a}}ndez del R{\'{i}}o and Mark Wiebe and Pearu Peterson and Pierre
		  G{\'{e}}rard-Marchant and Kevin Sheppard and Tyler Reddy and Warren Weckesser and Hameer Abbasi and
		  Christoph Gohlke and Travis E. Oliphant},
  year		= 2020,
  month		= sep,
  journal	= {Nature},
  volume	= 585,
  number	= 7825,
  pages		= {357--362},
  doi		= {10.1038/s41586-020-2649-2},
  publisher	= {Springer Science and Business Media {LLC}},
  url		= {https://doi.org/10.1038/s41586-020-2649-2}
}

@Misc{		  isabelle:codegen:2021,
  title		= {Code generation from {Isabelle/HOL} theories},
  author	= {Haftmann, Florian and Bulwahn, Lukas},
  journal	= {Part of the Isabelle documentation},
  url		= {http://isabelle.in.tum.de/doc/codegen.pdf},
  year		= 2021
}

@Booklet{	  bsi:50128:2014,
  abstract	= {This European Standard is part of a group of related standards. The others are EN 50126-1:1999
		  "Railway applications -- The specification and demonstration of Reliability, Availability,
		  Maintainability and Safety (RAMS) -- Part 1: Basic requirements and generic process -- and EN
		  50129:2003 "Railway applications -- Communication, signalling and processing systems -- Safety related
		  electronic systems for signalling". EN 50126-1 addresses system issues on the widest scale, while EN
		  50129 addresses the approval process for individual systems which can exist within the overall railway
		  control and protection system. This European Standard concentrates on the methods which need to be
		  used in order to provide software which meets the demands for safety integrity which are placed upon
		  it by these wider considerations. This European Standard provides a set of requirements with which the
		  development, deployment and maintenance of any safety-related software intended for railway control
		  and protection applications shall comply. It defines requirements concerning organisational structure,
		  the relationship between organisations and division of responsibility involved in the development,
		  deployment and maintenanceactivities.},
  institution	= {British Standards Institute (BSI)},
  date		= {2014-04},
  keywords	= {CENELEC},
  series	= {British Standards Publication},
  title		= {BS EN 50128:2011: Railway applications -- Communication, signalling and processing systems --
		  Software for railway control and protecting systems}
}

@Booklet{	  cc:cc:2017,
  institution	= {Common Criteria},
  date		= 2017,
  note		= {Available at \url{https://www.commoncriteriaportal.org/cc/}.},
  title		= {Common Criteria for Information Technology Security Evaluation (Version 3.1, Release 5)}
}

@InBook{	  carlini.ea:adversarial:2017,
  author	= {Carlini, Nicholas and Wagner, David},
  title		= {Adversarial Examples Are Not Easily Detected: Bypassing Ten Detection Methods},
  year		= 2017,
  isbn		= 9781450352024,
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  url		= {https://doi.org/10.1145/3128572.3140444},
  abstract	= {Neural networks are known to be vulnerable to adversarial examples: inputs that are close to natural
		  inputs but classified incorrectly. In order to better understand the space of adversarial examples, we
		  survey ten recent proposals that are designed for detection and compare their efficacy. We show that
		  all can be defeated by constructing new loss functions. We conclude that adversarial examples are
		  significantly harder to detect than previously appreciated, and the properties believed to be
		  intrinsic to adversarial examples are in fact not. Finally, we propose several simple guidelines for
		  evaluating future proposed defenses.},
  booktitle	= {Artificial Intelligence and Security},
  pages		= {3--14},
  numpages	= 12
}

@InProceedings{	  katz.ea:reluplex:2017,
  author	= {Guy Katz and Clark W. Barrett and David L. Dill and Kyle Julian and Mykel J. Kochenderfer},
  editor	= {Rupak Majumdar and Viktor Kuncak},
  title		= {Reluplex: An Efficient {SMT} Solver for Verifying Deep Neural Networks},
  booktitle	= {CAV},
  series	= {LNCS 10426},
  pages		= {97--117},
  publisher	= {Springer},
  year		= 2017,
  doi		= {10.1007/978-3-319-63387-9\_5}
}

@Article{	  matichuk.ea:eisbach:2016,
  doi		= {10.1007/s10817-015-9360-2},
  month		= mar,
  paperurl	= {https://trustworthy.systems/publications/nicta_full_text/8465.pdf},
  journal	= {Journal of Automated Reasoning},
  year		= 2016,
  keywords	= {isabelle, eisbach, proof automation, sel4, l4.verified},
  volume	= 56,
  title		= {{Eisbach}: A Proof Method Language for {Isabelle}},
  number	= 3,
  author	= {Matichuk, Daniel and Murray, Toby and Wenzel, Makarius},
  pages		= {261--282}
}

@InCollection{	  brucker.ea:feedforward-nn-verification:2023,
  abstract	= {Neural networks are being used successfully to solve classification problems, e.g., for detecting
		  objects in images. It is well known that neural networks are susceptible if small changes applied to
		  their input result in misclassification. Situations in which such a slight input change, often hardly
		  noticeable by a human expert, results in a misclassification are called adversarial attacks. Such
		  attacks can be life-threatening if, for example, they occur in image classification systems used in
		  autonomous cars or medical diagnosis. Systems employing neural networks, e.g., for safety or security
		  critical functionality, are a particular challenge for formal verification, which usually expects a
		  program (e.g., given as source code in a programming language). Such a program does, per se, not exist
		  for neural networks. In this paper, we address this challenge by presenting a formal embed- ding of
		  feedforward neural networks into Isabelle/HOL, together with a discussion of properties that are
		  desirable for neural networks in critical applications. Our Isabelle-based prototype can import neural
		  networks trained in TensorFlow, and we demonstrate our approach using a neural network trained for the
		  classification of digits.
		  
		  },
  keywords	= {Neural network, Deep Learning, Classification Network, Feedforward Network, Verification,
		  {Isabelle/HOL}},
  location	= {L{\"u}beck, Germany},
  author	= {Achim D. Brucker and Amy Stell},
  booktitle	= {Formal Methods (FM 2023)},
  language	= {english},
  publisher	= pub-springer,
  address	= pub-springer:adr,
  series	= s-lncs,
  editor	= {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker},
  title		= {Verifying Feedforward Neural Networks for Classification in {Isabelle/HOL}},
  classification= {conference},
  areas		= {formal methods, software engineering},
  public	= {yes},
  year		= 2023,
  isbn		= {978-3-642-38915-3},
  pdf		= {http://www.brucker.ch/bibliography/download/2023/brucker.ea-feedforward-nn-verification-2023.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-feedforward-nn-verification-2023}
}

@Book{		  ratz:inclusion:1997,
  author	= {Ratz, Dietmar},
  year		= 1997,
  title		= {Inclusion isotone extended interval arithmetic. A toolbox update},
  language	= {english},
  note		= {Karlsruhe 1996. (Berichte aus dem Forschungsschwerpunkt Computerarithmetik, Intervallrechnung und
		  Numerische Algorithmen mit Ergebnisverifikation. 1996,5.)},
  doi		= {10.5445/IR/67997}
}

@Book{		  moore.ea:introduction:2009,
  author	= {Moore, Ramon E. and Kearfott, R. Baker and Cloud, Michael J.},
  title		= {Introduction to Interval Analysis},
  year		= 2009,
  isbn		= 0898716691,
  publisher	= {Society for Industrial and Applied Mathematics},
  address	= {USA},
  abstract	= {This unique book provides an introduction to a subject whose use has steadily increased over the past
		  40 years. An update of Ramon Moore s previous books on the topic, it provides broad coverage of the
		  subject as well as the historical perspective of one of the originators of modern interval analysis.
		  The authors provide a hands-on introduction to INTLAB, a high-quality, comprehensive MATLAB toolbox
		  for interval computations, making this the first interval analysis book that does with INTLAB what
		  general numerical analysis texts do with MATLAB. Readers will find the following features of interest:
		  elementary motivating examples and notes that help maximize the reader s chance of success in applying
		  the techniques; exercises and hands-on MATLAB-based examples woven into the text; INTLAB-based
		  examples and explanations integrated into the text, along with a comprehensive set of exercises and
		  solutions, and an appendix with INTLAB commands; an extensive bibliography and appendices that will
		  continue to be valuable resources once the reader is familiar with the subject; and a Web page with
		  links to computational tools and other resources of interest. Audience: Introduction to Interval
		  Analysis will be valuable to engineers and scientists interested in scientific computation, especially
		  in reliability, effects of roundoff error, and automatic verification of results. The introductory
		  material is particularly important for experts in global optimization and constraint solution
		  algorithms. This book is suitable for introducing the subject to students in these areas. Contents:
		  Preface; Chapter 1: Introduction; Chapter 2: The Interval Number System; Chapter 3: First Applications
		  of Interval Arithmetic; Chapter 4: Further Properties of Interval Arithmetic; Chapter 5: Introduction
		  to Interval Functions; Chapter 6: Interval Sequences; Chapter 7: Interval Matrices; Chapter 8:
		  Interval Newton Methods; Chapter 9: Integration of Interval Functions; Chapter 10: Integral and
		  Differential Equations; Chapter 11: Applications; Appendix A: Sets and Functions; Appendix B:
		  Formulary; Appendix C: Hints for Selected Exercises; Appendix D: Internet Resources; Appendix E:
		  INTLAB Commands and Functions; References; Index.}
}

@Article{         harapanahalli.ea:toolbox:2023,
  author        = {Akash Harapanahalli and Saber Jafarpour and Samuel Coogan},
  title         = {A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural
                  Network Controlled Systems},
  journal       = {CoRR},
  volume        = {abs/2306.15340},
  year          = 2023,
  url           = {https://doi.org/10.48550/arXiv.2306.15340},
  doi           = {10.48550/ARXIV.2306.15340},
  eprinttype    = {arXiv},
  eprint        = {2306.15340},
  timestamp     = {Fri, 30 Jun 2023 15:53:15 +0200},
  biburl        = {https://dblp.org/rec/journals/corr/abs-2306-15340.bib},
  bibsource     = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{   wang.ea:formal-security:2018,
  author        = {Wang, Shiqi and Pei, Kexin and Whitehouse, Justin and Yang, Junfeng and Jana, Suman},
  title         = {Formal Security Analysis of Neural Networks Using Symbolic Intervals},
  year          = 2018,
  isbn          = 9781931971461,
  publisher     = {USENIX Association},
  address       = {USA},
  abstract      = {Due to the increasing deployment of Deep Neural Networks (DNNs) in real-world security-critical
                  domains including autonomous vehicles and collision avoidance systems, formally checking security
                  properties of DNNs, especially under different attacker capabilities, is becoming crucial. Most
                  existing security testing techniques for DNNs try to find adversarial examples without providing any                 
                  formal security guarantees about the nonexistence of such adversarial examples. Recently, several
                  projects have used different types of Satisfiability Modulo Theory (SMT) solvers to formally check
                  security properties of DNNs. However, all of these approaches are limited by the high overhead caused                
                  by the solver.In this paper, we present a new direction for formally checking security properties of                 
                  DNNs without using SMT solvers. Instead, we leverage interval arithmetic to compute rigorous bounds on
                  the DNN outputs. Our approach, unlike existing solver-based approaches, is easily parallelizable. We 
                  further present symbolic interval analysis along with several other optimizations to minimize
                  overestimations of output bounds.We design, implement, and evaluate our approach as part of ReluVal, a
                  system for formally checking security properties of Relu-based DNNs. Our extensive empirical results
                  show that ReluVal outperforms Reluplex, a state-of-the-art solver-based system, by 200 times on
                  average. On a single 8-core machine without GPUs, within 4 hours, ReluVal is able to verify a security
                  property that Reluplex deemed inconclusive due to timeout after running for more than 5 days. Our
                  experiments demonstrate that symbolic interval analysis is a promising new direction towards
                  rigorously analyzing different security properties of DNNs.},
  booktitle     = {Proceedings of the 27th USENIX Conference on Security Symposium},
  pages         = {1599--1614},
  numpages      = 16,
  location      = {Baltimore, MD, USA},
  series        = {SEC'18}
}

@InProceedings{   brucker.ea:formally:2024,
  author        = {Achim D. Brucker and Teddy Cameron-Burke and Amy Stell},
  title         = {Formally Verified Interval Arithmetic and Its Application to
                  Program Verification},
  booktitle     = {13th {IEEE/ACM} International Conference on Formal Methods in
                  Software Engineering (FormaliSE 2024)},
  pages         = {},
  publisher     = {{IEEE}},
  year          = 2024,
  doi           = {}
}
