use DocumenterCitations for bibliography

JuliaReach · Jan 25, 2025 · 6163a38 · 6163a38
1 parent aac8b9d
commit 6163a38
Show file tree

Hide file tree

Showing 9 changed files with 113 additions and 25 deletions.
diff --git a/docs/Project.toml b/docs/Project.toml
@@ -1,5 +1,7 @@
 [deps]
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244"
 
 [compat]
 Documenter = "1"
+DocumenterCitations = "1.3"
diff --git a/docs/make.jl b/docs/make.jl
@@ -1,18 +1,23 @@
-using Documenter, NeuralNetworkReachability
+using Documenter, NeuralNetworkReachability, DocumenterCitations
 
 DocMeta.setdocmeta!(NeuralNetworkReachability, :DocTestSetup,
                     :(using NeuralNetworkReachability); recursive=true)
 
+bib = CitationBibliography(joinpath(@__DIR__, "src", "refs.bib"); style=:alpha)
+
 makedocs(; sitename="NeuralNetworkReachability.jl",
          modules=[NeuralNetworkReachability],
          format=Documenter.HTML(; prettyurls=get(ENV, "CI", nothing) == "true",
-                                collapselevel=1, assets=["assets/aligned.css"]),
+                                collapselevel=1,
+                                assets=["assets/aligned.css", "assets/citations.css"]),
          pagesonly=true,
+         plugins=[bib],
          pages=["Home" => "index.md",
                 "Library" => Any["ForwardAlgorithms" => "lib/ForwardAlgorithms.md",
                                  "BackwardAlgorithms" => "lib/BackwardAlgorithms.md",
                                  "BidirectionalAlgorithms" => "lib/BidirectionalAlgorithms.md",
                                  "Util" => "lib/Util.md"],
+                "Bibliography" => "bibliography.md",
                 "About" => "about.md"])
 
 deploydocs(; repo="github.com/JuliaReach/NeuralNetworkReachability.jl.git",

diff --git a/docs/src/assets/citations.css b/docs/src/assets/citations.css
@@ -0,0 +1,17 @@
+.citation dl {
+  display: grid;
+  grid-template-columns: max-content auto; }
+.citation dt {
+  grid-column-start: 1; }
+.citation dd {
+  grid-column-start: 2;
+  margin-bottom: 0.75em; }
+.citation ul {
+ padding: 0 0 2.25em 0;
+ margin: 0;
+ list-style: none !important;}
+.citation ul li {
+ text-indent: -2.25em;
+ margin: 0.33em 0.5em 0.5em 2.25em;}
+.citation ol li {
+ padding-left:0.75em;}
diff --git a/docs/src/bibliography.md b/docs/src/bibliography.md
@@ -0,0 +1,4 @@
+# Bibliography
+
+```@bibliography
+```
diff --git a/docs/src/refs.bib b/docs/src/refs.bib
@@ -0,0 +1,77 @@
+
+@inproceedings{GehrMDTCV18,
+  author       = {Timon Gehr and
+                  Matthew Mirman and
+                  Dana Drachsler{-}Cohen and
+                  Petar Tsankov and
+                  Swarat Chaudhuri and
+                  Martin T. Vechev},
+  title        = {{AI2:} Safety and Robustness Certification of Neural Networks with
+                  Abstract Interpretation},
+  booktitle    = {2018 {IEEE} Symposium on Security and Privacy, {SP} 2018, Proceedings,
+                  21-23 May 2018, San Francisco, California, {USA}},
+  pages        = {3--18},
+  publisher    = {{IEEE} Computer Society},
+  year         = {2018},
+  url          = {https://doi.org/10.1109/SP.2018.00058},
+  doi          = {10.1109/SP.2018.00058},
+  timestamp    = {Fri, 24 Mar 2023 00:03:11 +0100},
+  biburl       = {https://dblp.org/rec/conf/sp/GehrMDTCV18.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{SinghGMPV18,
+  author       = {Gagandeep Singh and
+                  Timon Gehr and
+                  Matthew Mirman and
+                  Markus P{\"{u}}schel and
+                  Martin T. Vechev},
+  editor       = {Samy Bengio and
+                  Hanna M. Wallach and
+                  Hugo Larochelle and
+                  Kristen Grauman and
+                  Nicol{\`{o}} Cesa{-}Bianchi and
+                  Roman Garnett},
+  title        = {Fast and Effective Robustness Certification},
+  booktitle    = {Advances in Neural Information Processing Systems ({NeurIPS})},
+  pages        = {10825--10836},
+  year         = {2018},
+  url          = {https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html}
+}
+
+@inproceedings{IvanovWAPL19,
+  author       = {Radoslav Ivanov and
+                  James Weimer and
+                  Rajeev Alur and
+                  George J. Pappas and
+                  Insup Lee},
+  editor       = {Necmiye Ozay and
+                  Pavithra Prabhakar},
+  title        = {Verisig: verifying safety properties of hybrid systems with neural
+                  network controllers},
+  booktitle    = {Hybrid Systems: Computation and Control ({HSCC})},
+  pages        = {169--178},
+  publisher    = {{ACM}},
+  year         = {2019},
+  url          = {https://doi.org/10.1145/3302504.3311806},
+  doi          = {10.1145/3302504.3311806}
+}
+
+@inproceedings{Kochdumper0AB23,
+  author       = {Niklas Kochdumper and
+                  Christian Schilling and
+                  Matthias Althoff and
+                  Stanley Bak},
+  editor       = {Kristin Yvonne Rozier and
+                  Swarat Chaudhuri},
+  title        = {Open- and Closed-Loop Neural Network Verification Using Polynomial
+                  Zonotopes},
+  booktitle    = {{NASA} Formal Methods ({NFM})},
+  series       = {LNCS},
+  volume       = {13903},
+  pages        = {16--36},
+  publisher    = {Springer},
+  year         = {2023},
+  url          = {https://doi.org/10.1007/978-3-031-33170-1_2},
+  doi          = {10.1007/978-3-031-33170-1_2}
+}
diff --git a/src/ForwardAlgorithms/AI2.jl b/src/ForwardAlgorithms/AI2.jl
@@ -2,31 +2,25 @@
     AI2Box <: AI2
 
 AI2 forward algorithm for ReLU activation functions based on abstract
-interpretation with the interval domain from [1].
+interpretation with the interval domain from [GehrMDTCV18](@citet).
 
 ### Notes
 
 This algorithm is less precise than [`BoxForward`](@ref) because it abstracts
 after every step, including the affine map.
-
-[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks
-with abstract interpretation*, SP 2018.
 """
 struct AI2Box <: ForwardAlgorithm end
 
 """
     AI2Zonotope <: AI2
 
 AI2 forward algorithm for ReLU activation functions based on abstract
-interpretation with the zonotope domain from [1].
+interpretation with the zonotope domain from [GehrMDTCV18](@citet).
 
 ### Fields
 
 - `join_algorithm` -- (optional; default: `"join"`) algorithm to compute the
                       join of two zonotopes
-
-[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks
-with abstract interpretation*, SP 2018.
 """
 struct AI2Zonotope{S} <: ForwardAlgorithm
     join_algorithm::S
@@ -39,10 +33,7 @@ AI2Zonotope() = AI2Zonotope("join")
     AI2Polytope <: AI2
 
 AI2 forward algorithm for ReLU activation functions based on abstract
-interpretation with the polytope domain from [1].
-
-[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks
-with abstract interpretation*, SP 2018.
+interpretation with the polytope domain from [GehrMDTCV18](@citet).
 """
 struct AI2Polytope <: ForwardAlgorithm end
 

diff --git a/src/ForwardAlgorithms/DeepZ.jl b/src/ForwardAlgorithms/DeepZ.jl
@@ -2,9 +2,7 @@
     DeepZ <: ForwardAlgorithm
 
 Forward algorithm based on zonotopes for ReLU, sigmoid, and tanh activation
-functions from [1].
-
-[1]: Singh et al.: *Fast and Effective Robustness Certification*, NeurIPS 2018.
+functions from [SinghGMPV18](@citet).
 """
 struct DeepZ <: ForwardAlgorithm end
 

diff --git a/src/ForwardAlgorithms/PolyZonoForward.jl b/src/ForwardAlgorithms/PolyZonoForward.jl
@@ -34,7 +34,7 @@ struct TaylorExpansionQuadratic <: QuadraticApproximation end
     PolyZonoForward{A<:PolynomialApproximation,N,R} <: ForwardAlgorithm
 
 Forward algorithm based on poynomial zonotopes via polynomial approximation from
-[1].
+[Kochdumper0AB23](@citet).
 
 ### Fields
 
@@ -54,9 +54,6 @@ The default constructor takes keyword arguments with the following defaults:
 
 See the subtypes of `PolynomialApproximation` for available polynomial
 approximation methods.
-
-[1]: Kochdumper et al.: *Open- and closed-loop neural network verification using
-polynomial zonotopes*, NFM 2023.
 """
 struct PolyZonoForward{A<:PolynomialApproximation,O,R} <: ForwardAlgorithm
     polynomial_approximation::A

diff --git a/src/ForwardAlgorithms/Verisig.jl b/src/ForwardAlgorithms/Verisig.jl
@@ -1,7 +1,7 @@
 """
     Verisig{R} <: ForwardAlgorithm
 
-Forward algorithm for sigmoid and tanh activation functions from [1].
+Forward algorithm for sigmoid and tanh activation functions from [IvanovWAPL19](@citet).
 
 ### Fields
 
@@ -13,9 +13,6 @@ The implementation is known to be unsound in some cases.
 
 The implementation currently only supports neural networks with a single hidden
 layer.
-
-[1] Ivanov et al.: *Verisig: verifying safety properties of hybrid systems with
-neural network controllers*, HSCC 2019.
 """
 struct Verisig{R} <: ForwardAlgorithm
     algo::R