This tool won the best reward award for ARCH20 competition.
Similar tools: CORA, etc.

Install

In [ ]:
# %%sh
# cd res/
# git clone https://github.com/JuliaReach/ARCH2020_NLN_RE.git

Verify Non-linear Benchmarks

In [1]:
using Pkg
Pkg.activate(@__DIR__)
Pkg.instantiate()
 Activating environment at `~/Research/blogs/notebooks/Verifiable AI/res/ARCH2020_NLN_RE/Project.toml`
In [2]:
global io = open("res.csv", "w")
Out[2]:
IOStream(<file res.csv>)
In [3]:
include("models/VanDerPol/vanderpol_benchmark.jl")
(1/1) benchmarking "CVDP20"...
  (1/2) benchmarking "μ=2.0"...
  done (took 34.396497393 seconds)
  (2/2) benchmarking "μ=1.0"...
  done (took 6.747025392 seconds)
done (took 42.797715139 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "CVDP20" => 2-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "μ=2.0" => TrialEstimate(32.963 s)
	  "μ=1.0" => TrialEstimate(334.900 ms)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "CVDP20" => 2-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "μ=2.0" => TrialEstimate(32.963 s)
	  "μ=1.0" => TrialEstimate(367.752 ms)
In [4]:
# Production-destruction benchmark
include("models/ProdDestruct/prod_destruct_benchmark.jl")
volume final box, case I : 3.3e-20
volume final box, case P : 5.3e-21
volume final box, case IP : 1.0e-20
(1/1) benchmarking "PRDE20"...
  (1/3) benchmarking "I"...
  done (took 6.687252579 seconds)
  (2/3) benchmarking "IP"...
  done (took 7.801292505 seconds)
  (3/3) benchmarking "P"...
  done (took 9.715274608 seconds)
done (took 25.740959423 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "PRDE20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "I" => TrialEstimate(1.562 s)
	  "IP" => TrialEstimate(2.889 s)
	  "P" => TrialEstimate(4.035 s)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "PRDE20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "I" => TrialEstimate(1.588 s)
	  "IP" => TrialEstimate(3.114 s)
	  "P" => TrialEstimate(4.049 s)
In [5]:
# Laub-Loomis benchmark
include("models/LaubLoomis/laubloomis_benchmark.jl")
width of final box, case W=0.01 : 0.00422669680166976
width of final box, case W=0.05: 0.017462225836897716
width of final box, case W=0.1 : 0.03362699736716124
(1/1) benchmarking "LALO20"...
  (1/3) benchmarking "W=0.01"...
  done (took 7.57624038 seconds)
  (2/3) benchmarking "W=0.1"...
  done (took 7.795454151 seconds)
  (3/3) benchmarking "W=0.05"...
  done (took 7.913053309 seconds)
done (took 24.867507693 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "LALO20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "W=0.01" => TrialEstimate(916.856 ms)
	  "W=0.1" => TrialEstimate(1.153 s)
	  "W=0.05" => TrialEstimate(1.180 s)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "LALO20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "W=0.01" => TrialEstimate(986.492 ms)
	  "W=0.1" => TrialEstimate(1.195 s)
	  "W=0.05" => TrialEstimate(1.221 s)
In [6]:
# Quadrotor benchmark
include("models/Quadrotor/quadrotor_benchmark.jl")
Validate property, case Δ=0.1 : true
Validate property, case Δ=0.4 : true
Validate property, case Δ=0.8 : false
(1/1) benchmarking "QUAD20"...
  (1/3) benchmarking "Δ=0.1"...
  done (took 7.482609231 seconds)
  (2/3) benchmarking "Δ=0.4"...
  done (took 7.457505771 seconds)
  (3/3) benchmarking "Δ=0.8"...
  done (took 7.467502425 seconds)
done (took 24.139690623 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "QUAD20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "Δ=0.1" => TrialEstimate(1.845 s)
	  "Δ=0.4" => TrialEstimate(1.368 s)
	  "Δ=0.8" => TrialEstimate(1.391 s)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "QUAD20" => 3-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "Δ=0.1" => TrialEstimate(1.910 s)
	  "Δ=0.4" => TrialEstimate(1.411 s)
	  "Δ=0.8" => TrialEstimate(1.421 s)
In [7]:
# Lotka-Volterra tangential crossing benchmark
include("models/LotkaVolterra/lotka_volterra_benchmark.jl")
tmin = 2.6607663522539795
tmax = 2.843324138086564
tmax - tmin = 0.18255778583258442
Final area, case  : 0.002201292698526464
Time spent in guard, case  : 0.18255778583258442
(1/1) benchmarking "LOVO20"...
  (1/1) benchmarking ""...
  done (took 7.94730342 seconds)
done (took 9.755495225 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "LOVO20" => 1-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "" => TrialEstimate(6.123 s)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "LOVO20" => 1-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "" => TrialEstimate(6.123 s)
In [8]:
# Spacecraft benchmark
include("models/Spacecraft/spacecraft_benchmark.jl")
Line of sight property: true
Velocity constraint property true
Target avoidance property: true
(1/1) benchmarking "SPRE20"...
  (1/1) benchmarking ""...
  done (took 17.989037294 seconds)
done (took 20.02641975 seconds)
minimum time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "SPRE20" => 1-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "" => TrialEstimate(15.918 s)
median time for each benchmark:
1-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "SPRE20" => 1-element BenchmarkTools.BenchmarkGroup:
	  tags: []
	  "" => TrialEstimate(15.918 s)