add files

.github/workflows/SpellCheck.yml

@@ -0,0 +1,13 @@
+name: Spell Check
+
+on: [pull_request]
+
+jobs:
+  typos-check:
+    name: check spelling
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Actions Repository
+        uses: actions/checkout@v4
+      - name: Check spelling
+        uses: crate-ci/typos@master

.github/workflows/TagBot.yml

@@ -14,3 +14,4 @@ jobs:
       - uses: JuliaRegistries/TagBot@v1
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
+          ssh: ${{ secrets.DOCUMENTER_KEY }}

.github/workflows/ci_PR.yml

@@ -22,7 +22,7 @@ jobs:
         arch:
           - x64
         include:
-          - version: '1.2'  # test on oldest supported version
+          - version: '1.6'  # test on oldest supported version
             arch: x64
             os: ubuntu-latest
     env:

.gitignore

@@ -19,3 +19,6 @@ docs/site/
 .vscode
 
 Manifest.toml
+
+*.pdf
+*.png

.typos.toml

@@ -0,0 +1,3 @@
+[default.extend-words]
+# do not correct the following strings:
+BA = "BA"

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2019 JuliaReach
+Copyright (c) 2023 JuliaReach
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

Project.toml

@@ -1,8 +1,19 @@
-name = "JuliaReachTemplatePkg"
-uuid = "2b714139-d377-45b9-9f15-0355f7430025"
+name = "NeuralNetworkReachability"
+uuid = "5de1e908-2f08-45bf-a571-ac88a54f7e7f"
 version = "0.1.0"
 
 [deps]
+ControllerFormats = "02ac4b2c-022a-44aa-84a5-ea45a5754bcc"
+LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043"
+LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
+ReachabilityBase = "379f33d0-9447-4353-bd03-d664070e549f"
+Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
+Requires = "ae029012-a4dd-5104-9daa-d747884805df"
 
 [compat]
-julia = "1"
+ControllerFormats = "0.2"
+LazySets = "2.11.1"
+ReachabilityBase = "0.2.1"
+Reexport = "0.2, 1"
+Requires = "0.5, 1"
+julia = "1.6"

README.md

@@ -1,47 +1,19 @@
-# JuliaReachTemplatePkg.jl
+# NeuralNetworkReachability.jl
 
 | **Documentation** | **Status** | **Community** | **License** |
 |:-----------------:|:----------:|:-------------:|:-----------:|
-| [![docs-dev][dev-img]][dev-url] | [![CI][ci-img]][ci-url] [![codecov][cov-img]][cov-url] | [![gitter][chat-img]][chat-url] | [![license][lic-img]][lic-url] |
+| [![docs-dev][dev-img]][dev-url] | [![CI][ci-img]][ci-url] [![codecov][cov-img]][cov-url] | [![zulip][chat-img]][chat-url] | [![license][lic-img]][lic-url] |
 
 [dev-img]: https://img.shields.io/badge/docs-latest-blue.svg
-[dev-url]: https://juliareach.github.io/JuliaReachTemplatePkg.jl/dev/
-[ci-img]: https://github.com/JuliaReach/JuliaReachTemplatePkg.jl/workflows/CI/badge.svg
-[ci-url]: https://github.com/JuliaReach/JuliaReachTemplatePkg.jl/actions/workflows/ci.yml
-[cov-img]: https://codecov.io/github/JuliaReach/JuliaReachTemplatePkg.jl/coverage.svg
-[cov-url]: https://app.codecov.io/github/JuliaReach/JuliaReachTemplatePkg.jl
+[dev-url]: https://juliareach.github.io/NeuralNetworkReachability.jl/dev/
+[ci-img]: https://github.com/JuliaReach/NeuralNetworkReachability.jl/workflows/CI/badge.svg
+[ci-url]: https://github.com/JuliaReach/NeuralNetworkReachability.jl/actions/workflows/ci.yml
+[cov-img]: https://codecov.io/github/JuliaReach/NeuralNetworkReachability.jl/coverage.svg
+[cov-url]: https://app.codecov.io/github/JuliaReach/NeuralNetworkReachability.jl
 [chat-img]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg
 [chat-url]: https://julialang.zulipchat.com/#narrow/stream/278609-juliareach
 [lic-img]: https://img.shields.io/github/license/mashape/apistatus.svg
-[lic-url]: https://github.com/JuliaReach/JuliaReachTemplatePkg.jl/blob/master/LICENSE
+[lic-url]: https://github.com/JuliaReach/NeuralNetworkReachability.jl/blob/master/LICENSE
 
-`JuliaReachTemplatePkg` is a [Julia](http://julialang.org) template package for
-the JuliaReach ecosystem.
-
-## Installing
-
-This package requires Julia v1.0 or later.
-We refer to the [official documentation](https://julialang.org/downloads) on how
-to install and run Julia on your system.
-
-Depending on your needs, choose an appropriate command from the following list
-and enter it in Julia's REPL.
-To activate the `pkg` mode, type `]` (and to leave it, type `<backspace>`).
-
-#### [Install the latest release version](https://pkgdocs.julialang.org/v1/managing-packages/#Adding-registered-packages-1)
-
-```julia
-pkg> add JuliaReachTemplatePkg
-```
-
-#### Install the latest development version
-
-```julia
-pkg> add JuliaReachTemplatePkg#master
-```
-
-#### [Clone the package for development](https://pkgdocs.julialang.org/v1/managing-packages/#developing)
-
-```julia
-pkg> dev JuliaReachTemplatePkg
-```
+`NeuralNetworkReachability.jl` is a [Julia](http://julialang.org) package to symbolically analyze
+neural networks.

docs/Project.toml

@@ -1,2 +1,5 @@
 [deps]
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+
+[compat]
+Documenter = "1"

docs/make.jl

@@ -1,15 +1,18 @@
-using Documenter, JuliaReachTemplatePkg
+using Documenter, NeuralNetworkReachability
 
-DocMeta.setdocmeta!(JuliaReachTemplatePkg, :DocTestSetup,
-                    :(using JuliaReachTemplatePkg); recursive=true)
+DocMeta.setdocmeta!(NeuralNetworkReachability, :DocTestSetup,
+                    :(using NeuralNetworkReachability); recursive=true)
 
-makedocs(; sitename="JuliaReachTemplatePkg.jl",
-         modules=[JuliaReachTemplatePkg],
+makedocs(; sitename="NeuralNetworkReachability.jl",
+         modules=[NeuralNetworkReachability],
          format=Documenter.HTML(; prettyurls=get(ENV, "CI", nothing) == "true",
-                                assets=["assets/aligned.css"]),
+                                collapselevel=1, assets=["assets/aligned.css"]),
+         pagesonly=true,
          pages=["Home" => "index.md",
-                "About" => "about.md"],
-         strict=true)
+                "Library" => Any["ForwardAlgorithms" => "lib/ForwardAlgorithms.md",
+                                 "BackwardAlgorithms" => "lib/BackwardAlgorithms.md",
+                                 "BidirectionalAlgorithms" => "lib/BidirectionalAlgorithms.md"],
+                "About" => "about.md"])
 
-deploydocs(; repo="github.com/JuliaReach/JuliaReachTemplatePkg.jl.git",
+deploydocs(; repo="github.com/JuliaReach/NeuralNetworkReachability.jl.git",
            push_preview=true)

docs/src/about.md

@@ -13,7 +13,7 @@ If you like this package, consider contributing!
 
 [Creating an issue](https://docs.github.com/en/issues/tracking-your-work-with-issues/creating-an-issue) in
 the
-[JuliaReachTemplatePkg GitHub issue tracker](https://github.com/JuliaReach/JuliaReachTemplatePkg.jl/issues)
+[NeuralNetworkReachability GitHub issue tracker](https://github.com/JuliaReach/NeuralNetworkReachability.jl/issues)
 to report a bug, open a discussion about existing functionality, or suggest new
 functionality is appreciated.
 
@@ -53,7 +53,7 @@ To run the unit tests locally, you can do:
 ```julia
 julia> using Pkg
 
-julia> Pkg.test("JuliaReachTemplatePkg")
+julia> Pkg.test("NeuralNetworkReachability")
 ```
 
 We also advise adding new unit tests when adding new features to ensure
@@ -86,7 +86,7 @@ $ julia --color=yes docs/make.jl
 
 ## Credits
 
-Here we list the names of the maintainers of the `JuliaReachTemplatePkg.jl`
+Here we list the names of the maintainers of the `NeuralNetworkReachability.jl`
 library, as well as past and present contributors (in alphabetic order).
 
 ### Core developers

docs/src/index.md

@@ -1,12 +1,8 @@
-# JuliaReachTemplatePkg.jl
+# NeuralNetworkReachability.jl
 
-`JuliaReachTemplatePkg` is a [Julia](http://julialang.org) template package for
-the JuliaReach ecosystem.
-
-## Library Outline
+[NeuralNetworkReachability.jl](http://github.com/JuliaReach/NeuralNetworkReachability.jl) is a
+[Julia](http://julialang.org) package for reachability analysis of artificial neural networks.
 
 ```@contents
-Pages = [
-]
-Depth = 2
+Pages = ["index.md"]
 ```

docs/src/lib/BackwardAlgorithms.md

@@ -0,0 +1,19 @@
+# BackwardAlgorithms
+
+This section of the manual describes the module for backward algorithms.
+
+```@contents
+Pages = ["BackwardAlgorithms.md"]
+Depth = 3
+```
+
+```@meta
+CurrentModule = NeuralNetworkReachability.BackwardAlgorithms
+```
+
+```@docs
+BackwardAlgorithm
+PolyhedraBackward
+BoxBackward
+PartitioningLeakyReLU
+```

docs/src/lib/BidirectionalAlgorithms.md

@@ -0,0 +1,17 @@
+# BidirectionalAlgorithms
+
+This section of the manual describes the module for bidirectional algorithms.
+
+```@contents
+Pages = ["BidirectionalAlgorithms.md"]
+Depth = 3
+```
+
+```@meta
+CurrentModule = NeuralNetworkReachability.BidirectionalAlgorithms
+```
+
+```@docs
+BidirectionalAlgorithm
+SimpleBidirectional
+```

docs/src/lib/ForwardAlgorithms.md

@@ -0,0 +1,23 @@
+# ForwardAlgorithms
+
+This section of the manual describes the module for forward algorithms.
+
+```@contents
+Pages = ["ForwardAlgorithms.md"]
+Depth = 3
+```
+
+```@meta
+CurrentModule = NeuralNetworkReachability.ForwardAlgorithms
+```
+
+```@docs
+ForwardAlgorithm
+DefaultForward
+ConcreteForward
+LazyForward
+BoxForward
+SplitForward
+DeepZ
+Verisig
+```

src/BackwardAlgorithms/BackwardAlgorithm.jl

@@ -0,0 +1,8 @@
+"""
+BackwardAlgorithm
+
+Abstract supertype of backward algorithms.
+"""
+abstract type BackwardAlgorithm end
+
+remove_constraints(::BackwardAlgorithm, x) = false

src/BackwardAlgorithms/BackwardAlgorithms.jl

@@ -0,0 +1,22 @@
+module BackwardAlgorithms
+
+using ControllerFormats
+using LazySets
+using LazySets: affine_map_inverse
+using ReachabilityBase.Arrays: SingleEntryVector
+using ReachabilityBase.Comparison: _leq
+using ReachabilityBase.Iteration: BitvectorIterator
+using LinearAlgebra: Diagonal
+
+export backward,
+       PolyhedraBackward,
+       BoxBackward
+
+include("simplify_sets.jl")
+include("PartitioningLeakyReLU.jl")
+include("BackwardAlgorithm.jl")
+include("backward_default.jl")
+include("PolyhedraBackward.jl")
+include("BoxBackward.jl")
+
+end  # module

src/BackwardAlgorithms/BoxBackward.jl

@@ -0,0 +1,55 @@
+"""
+    BoxBackward <: BackwardAlgorithm
+
+Backward algorithm that uses a polyhedral approximation with axis-aligned
+linear constraints.
+"""
+struct BoxBackward <: BackwardAlgorithm end
+
+function backward(Y::LazySet, act::ReLU, ::BoxBackward)
+    return _backward_box(Y, act)
+end
+
+function backward(Y::UnionSetArray, act::ReLU, ::BoxBackward)
+    return _backward_box(Y, act)
+end
+
+function _backward_box(Y::LazySet{N}, ::ReLU) where {N}
+    n = dim(Y)
+
+    # intersect with nonnegative orthant
+    Q₊ = HPolyhedron([HalfSpace(SingleEntryVector(i, n, -one(N)), zero(N)) for i in 1:n])
+    Y₊ = intersection(Y, Q₊)
+    if isempty(Y₊)  # pre-image is empty if image was not nonnegative
+        return EmptySet{N}(dim(Y))
+    end
+
+    constraints = Vector{HalfSpace{N,SingleEntryVector{N}}}()
+    @inbounds for i in 1:n
+        e₊ = SingleEntryVector(i, n, one(N))
+        upper = ρ(e₊, Y₊)
+        if upper < N(Inf)
+            push!(constraints, HalfSpace(e₊, upper))
+        end
+
+        e₋ = SingleEntryVector(i, n, -one(N))
+        lower = -ρ(e₋, Y₊)
+        if !_leq(lower, zero(N))
+            push!(constraints, HalfSpace(e₋, lower))
+        end
+    end
+    if isempty(constraints)
+        return Universe{N}(n)
+    end
+    return HPolyhedron(constraints)
+end
+
+for T in (Sigmoid, LeakyReLU)
+    @eval begin
+        function backward(Y::AbstractHyperrectangle, act::$T, ::BoxBackward)
+            l = _inverse(low(Y), act)
+            h = _inverse(high(Y), act)
+            return Hyperrectangle(; low=l, high=h)
+        end
+    end
+end