use DocumenterCitations for bibliography

docs/Project.toml

@@ -1,6 +1,7 @@
 [deps]
 DisplayAs = "0b91fe84-8a4c-11e9-3e1d-67c38462b6d6"
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244"
 ExponentialUtilities = "d4d017d3-3776-5f7e-afef-a10c40355c18"
 IntervalArithmetic = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253"
 JLD2 = "033835bb-8acc-5ee8-8aae-3f567f8a3819"
@@ -16,6 +17,7 @@ Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7"
 [compat]
 DisplayAs = "0.1"
 Documenter = "1"
+DocumenterCitations = "1.3"
 ExponentialUtilities = "1"
 IntervalArithmetic = "=0.20.9"  # new versions require updates and are incompatible with dependencies
 JLD2 = "0.4 - 0.5"

docs/make.jl

@@ -1,11 +1,13 @@
-using Documenter, ReachabilityAnalysis
+using Documenter, ReachabilityAnalysis, DocumenterCitations
 
 # load optional packages for complete documentation
 import ExponentialUtilities
 
 DocMeta.setdocmeta!(ReachabilityAnalysis, :DocTestSetup,
                     :(using ReachabilityAnalysis); recursive=true)
 
+bib = CitationBibliography(joinpath(@__DIR__, "src", "refs.bib"); style=:alpha)
+
 # pass --fast as an argument to skip rebuilding the examples and running doctests
 const _FAST = findfirst(==("--fast"), ARGS) !== nothing
 
@@ -155,14 +157,13 @@ NONLINEAR_SOLVERS_API = [
 # Docs contents
 # ========================
 
-makedocs(;
-         format=Documenter.HTML(; prettyurls=haskey(ENV, "GITHUB_ACTIONS"),
-                                collapselevel=1,
-                                assets=["assets/aligned.css"]),
-         sitename="ReachabilityAnalysis.jl",
+makedocs(; sitename="ReachabilityAnalysis.jl",
          modules=[ReachabilityAnalysis],
-         #doctest=false,
+         format=Documenter.HTML(; prettyurls=get(ENV, "CI", nothing) == "true",
+                                collapselevel=1,
+                                assets=["assets/aligned.css", "assets/citations.css"]),
          pagesonly=true,
+         plugins=[bib],
          pages=[
                 #
                 "Overview" => "index.md",
@@ -230,10 +231,10 @@ makedocs(;
                                     #
                                     ],
                 "Frequently Asked Questions (FAQ)" => "man/faq.md",
-                "Bibliography" => "references.md", "How to contribute" => "about.md"
+                "Bibliography" => "bibliography.md",
+                "How to contribute" => "about.md"
                 #
                 ])
 
-# Deploy built documentation from Travis.
 deploydocs(; repo="github.com/JuliaReach/ReachabilityAnalysis.jl.git",
            push_preview=true)

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;}

docs/src/bibliography.md

@@ -0,0 +1,18 @@
+# [Bibliography](@id all_ref)
+
+This page includes references to the scientific works that we have applied
+throughout this library. Although the list is not meant to be exhaustive, we think
+it should give a solid starting place for those who want to explore further.
+
+If you use [ReachabilityAnalysis.jl](https://github.com/JuliaReach/ReachabilityAnalysis.jl) for your own work, please consider citing the
+appropriate original reference(s). We provide the BibTeX entries in each case.
+
+If you find that a reference here is missing, if you spot a typo or want to update
+a reference, do not hesitate to contact us by email, or open an issue. Sorting is alphabetic.
+
+```@bibliography
+```
+
+```@bibliography
+*
+```

docs/src/index.md

@@ -19,7 +19,7 @@ and safe machine learning.
 Below we briefly comment on a few remarkable problems where reachability is being
 applied. We refer to the technical literature for further applications;
 see [Bibliography](@ref all_ref) for a selection of papers to get you started!
-An up-to-date review with relevant references can be found in [[AFG20]](@ref).
+An up-to-date review with relevant references can be found in [AlthoffFG21](@citet).
 
 **Formal verification.** Determining whether a system is safe, i.e. to verify
 if it does not enter into a region of unsafe sets. Typical applications are

docs/src/lib/discretize.md

@@ -37,7 +37,7 @@ The state transition matrix of the linear ODE ``x'(t) = Ax(t) + u(t)`` at time
 ``δ > 0`` is ``Φ = e^{Aδ}``, hence the algorithms usually require to
 compute exponential matrices. There are distinct ways to compute the matrix
 exponential ``e^{Aδ}`` depending on the type of ``A``
-(see e.g. [^HIH08]). The available methods can be used through the (unexported) function `_exp`.
+(see, e.g., [Higham08](@cite)). The available methods can be used through the (unexported) function `_exp`.
 
 For high dimensional systems (typically `n > 2000`), computing the matrix exponential
 is expensive hence it is preferable to compute the action of the matrix exponential
@@ -55,7 +55,3 @@ ReachabilityAnalysis.Exponentiation.LazyExpAlg
 ReachabilityAnalysis.Exponentiation.IntervalExpAlg
 ReachabilityAnalysis.Exponentiation.PadeExpAlg
 ```
-
-## References
-
-[^HIH08]: Higham, Nicholas J. Functions of matrices: theory and computation. Society for Industrial and Applied Mathematics, 2008.

docs/src/man/algorithms/LGG09.md

@@ -7,7 +7,7 @@ CurrentModule = ReachabilityAnalysis
 
 ## Method
 
-In the following subsections we outline the method of [[LGG09]](@ref) to solve
+In the following subsections we outline the method of [LeGuernicG09](@citet) to solve
 linear set-based recurrences using support functions, first the homogeneous case
 and then the inhomogeneous case without wrapping effect.
 We also discuss the special case of real eigenvalues.
@@ -106,7 +106,7 @@ values. Hence each thread computes a subset of distinct rows of `ρℓ`.
 
 If the spectrum of the state matrix only has real eigenvalues, the sequence of
 support functions can be computed efficiently if we work with a template
-consisting of eigenvectors of ``Φ^T``. This idea is described in [[LGG09]](@ref)
+consisting of eigenvectors of ``Φ^T``. This idea is described in [LeGuernicG09](@citet)
 and we recall it here for convenience.
 
 The method stems from the fact that if ``(λ, d)`` is an eigenvalue-eigenvector

docs/src/man/algorithms/ORBIT.md

@@ -58,7 +58,7 @@ of ``Φ_1(u, δ)`` is available through the function
 
 (1) If the coefficients matrix ``A`` is invertible, then the integral is equivalent to computing ``A^{-1}(e^{Aδ} - I)``.
 
-(2) In general, ``Φ_1(u, δ)`` can be obtained as a sub-block of a larger matrix. See [[FRE11]](@ref) for details.
+(2) In general, ``Φ_1(u, δ)`` can be obtained as a sub-block of a larger matrix. See [FrehseGDCRLRGDM11](@citet) for details.
 
 Method (2) is the default method, although there are cases in which method (1) is more convenient.
 For example, if we are only interested in singleton inputs and ``A`` is invertible,

docs/src/man/benchmarks/filtered_oscillator.md

@@ -8,7 +8,7 @@ CurrentModule = ReachabilityAnalysis
 Scalability is very important in the applicability of a tool. For illustration
 purposes, in this section we consider the scalability of the hybrid reachability
 solver, using different algorithm choices, for the filtered switched oscillator
-model from [[FRE11]](@ref). The model consists of a two-dimensional switched oscillator
+model from [FrehseGDCRLRGDM11](@citet). The model consists of a two-dimensional switched oscillator
 and a parametric number of filters which are used to *smooth* the oscilllator's state.
 An interesting aspect of the model is that it is scalable: the total number of continuous
 variables can be made arbitrarily large. Moreover, this is a challenging benchmark
@@ -20,7 +20,7 @@ In this evaluation we consider that the number of filters ranges from 64 to 1024
 To measure the quality of the approximations, we consider the safety property given
 by ``y(t) < 0.5`` for all ``t ∈ [0, T]``.
 
-The filtered oscillator was also studied in [[BFFPS19]](@ref) to test the scalability
+The filtered oscillator was also studied in [BogomolovFFVPS18](@citet) to test the scalability
 of a new scheme that exploits the sparsity of the hybrid automaton to efficiently
 compute flowpipe-guard intersections. Such scheme is not considered in this section.
 

docs/src/man/clocked.md

@@ -11,7 +11,7 @@ So far we have focused on transitions that involve "spatial" variables.
 If the system under consideration has transitions governed by time variables,
 i.e. by variables whose dynamics are of the form ``t' = 1``, then decoupling the
 spatial variables with the clock variables gives a computational advantage.
-We refer to [[HG19]].
+We refer to [HakimB19](@citet).
 
 
 ![Hybrid automaton of the clocked model](../assets/clocked_simple_annotations.png)

docs/src/man/faq.md

@@ -17,7 +17,7 @@ we recommend the lecture notes of [Prof. Goran Frehse](https://sites.google.com/
 (DigiCosme Spring School, Paris, May 2016). Most up-to-date material related to reachability
 analysis can be found in journals, conference articles or in PhD theses.
 For a comprehensive review of different set propagation techniques for linear, nonlinear
-and hybrid systems see [[AFG20]](@ref). The article also contains a discussion of
+and hybrid systems see [AlthoffFG21](@citet). The article also contains a discussion of
 successful applications of reachability analysis to real-world problems.
 We refer to the [References](@ref all_ref) section of this manual for further links
 to the relevant literature.
@@ -27,7 +27,7 @@ to the relevant literature.
 The wiki [Related Tools](https://github.com/JuliaReach/ReachabilityAnalysis.jl/wiki/Related-Tools)
 contains an extensive list of pointers related to reachability analysis tools for
 dynamical systems. Languages and tools for hybrid systems design are described in the review article
-[[CPPSV06]](@ref) (a bit outdated with respect to the tools since it is of 2006).
+[CarloniPPS06](@cite) (a bit outdated with respect to the tools since it is of 2006).
 
 A subset of such tools has participated in recent editions of the Friendly Competition for Applied Reachability of Continuous and Hybrid Systems,
 [ARCH-COMP](https://cps-vo.org/group/ARCH). In alphabetic order: [Ariadne](http://www.ariadne-cps.org/), [CORA](https://tumcps.github.io/CORA/),
@@ -59,7 +59,7 @@ In our case, we began to develop the JuliaReach stack in 2017 and quickly adopte
 v0.5 [^v1]. Julia is a general-purpose programming language but it was conceived with high-performance scientific
 computing in mind, and it reconciles the two advantages of compiled and interpreted languages described above,
 as it comes with an interactive read-evaluate-print loop (REPL) front-end, but is JIT compiled to achieve performance
-that is competitive with compiled languages such as C [^BEKS17]. A distinctive feature of Julia is multiple dispatch
+that is competitive with compiled languages such as C [BezansonEKS17](@cite). A distinctive feature of Julia is multiple dispatch
 (i.e., the function to execute is chosen based on each argument type), which allows to write efficient machine code
 based on a given type, e.g., of the set. As additional features, Julia is platform independent,
 has an efficient interface to C and FORTRAN, is supported in Jupyter notebooks (the "Ju" in Jupyter is for *Ju*lia)
@@ -69,7 +69,7 @@ All this makes Julia an interesting programming language for writing a library f
 
 ### What is the wrapping effect?
 
-Quoting a famous paper by R. E. Moore [[M65]](@ref):
+Quoting the famous paper [Moore65](@citet):
 
 > Under the flow itself a box is carried after certain time into a set of points
 > which will in general not remain a box excepted for a few simple flows.
@@ -308,5 +308,3 @@ choice that intervals should belong to the `LazySets` type hierarchy.
 ## References
 
 [^v1]: Version 1.0 of the language was released in August 2018; see [this blog post](https://julialang.org/blog/2018/08/one-point-zero/).
-
-[^BEKS17]: Bezanson, J., Edelman, A., Karpinski, S., & Shah, V. B. (2017). Julia: A fresh approach to numerical computing. SIAM review, 59(1), 65-98.