diff --git a/bin/abcrown.sh b/bin/abcrown.sh
new file mode 100755
index 0000000000000000000000000000000000000000..d7cb228a896f40e1078b0b892f2d1ae9453623f1
--- /dev/null
+++ b/bin/abcrown.sh
@@ -0,0 +1,29 @@
+#!/usr/bin/env sh
+###########################################################################
+# #
+# This file is part of CAISAR. #
+# #
+# Copyright (C) 2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# You can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+###########################################################################
+
+if [ "$1" = "--version" ]; then
+ DIRNAME=$( dirname -- "$0"; )
+ $DIRNAME/findmodule.py "complete_verifier.abcrown" "dummy"
+else
+ python3 -m complete_verifier.abcrown "$@"
+fi
diff --git a/bin/dune b/bin/dune
index 45f3f6d1325e66f8f6a675268bdd0f51ebf1192d..b05c9abcfcdb286a5fae5f216698931c027652a7 100644
--- a/bin/dune
+++ b/bin/dune
@@ -3,4 +3,5 @@
(section bin)
(files
(findmodule.py as findmodule.py)
- (nnenum.sh as nnenum.sh)))
+ (nnenum.sh as nnenum.sh)
+ (abcrown.sh as abcrown.sh)))
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 133ab631e679fac8f51aa5bb8c9a4d26c3a542be..9de58f4b713a2569aca94757f6ac53b15b5c5860 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -98,6 +98,16 @@ command = "%e %{nnet-onnx} %f"
driver = "caisar_drivers/nnenum.drv"
use_at_auto_level = 1
+[ATP abcrown]
+name = "alpha-beta-CROWN"
+exec = "abcrown.sh"
+version_switch = "--version"
+version_regexp = "\\(dummy\\)"
+version_ok = "dummy"
+command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %t"
+driver = "caisar_drivers/abcrown.drv"
+use_at_auto_level = 1
+
[ATP saver]
name = "SAVer"
exec = "saver"
diff --git a/config/drivers/abcrown.drv b/config/drivers/abcrown.drv
new file mode 100644
index 0000000000000000000000000000000000000000..97b4a46a54f7bcdc3588f3c02f3d4a3d89c0d54d
--- /dev/null
+++ b/config/drivers/abcrown.drv
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Why3 driver for alpha-beta-CROWN *)
+
+prelude ";;; produced by alpha-beta-CROWN driver"
+
+import "vnnlib.gen"
+
+valid "^Result: safe"
+invalid "^Result: unsafe"
+timeout "^Time out!!!!!!!!"
+unknown "^Result: unknown" ""
diff --git a/config/dune b/config/dune
index 3a77163781bfdc0975e9f907538b6b8885c9779a..3bf2582372a65f9b69fd3891854e84d270a0dd46 100644
--- a/config/dune
+++ b/config/dune
@@ -11,5 +11,6 @@
(drivers/aimos.drv as drivers/aimos.drv)
(drivers/vnnlib.gen as drivers/vnnlib.gen)
(drivers/pyrat_vnnlib.drv as drivers/pyrat_vnnlib.drv)
- (drivers/nnenum.drv as drivers/nnenum.drv))
+ (drivers/nnenum.drv as drivers/nnenum.drv)
+ (drivers/abcrown.drv as drivers/abcrown.drv))
(package caisar))
diff --git a/src/prover.ml b/src/prover.ml
index ee7908d7b7913036b38bf5f512dbfa910b49eda4..bb9ee6ec95178f1d989df85d22d35fc1998b5596 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -27,9 +27,10 @@ type t =
| Aimos [@name "AIMOS"]
| CVC5 [@name "cvc5"]
| Nnenum [@name "nnenum"]
+ | ABCrown [@name "alpha-beta-CROWN"]
[@@deriving yojson, show]
-let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum ]
+let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum; ABCrown ]
let of_string prover =
let prover = String.lowercase_ascii prover in
@@ -40,6 +41,7 @@ let of_string prover =
| "aimos" -> Some Aimos
| "cvc5" -> Some CVC5
| "nnenum" -> Some Nnenum
+ | "abcrown" -> Some ABCrown
| _ -> None
let to_string = function
@@ -49,7 +51,8 @@ let to_string = function
| Aimos -> "AIMOS"
| CVC5 -> "CVC5"
| Nnenum -> "nnenum"
+ | ABCrown -> "alpha-beta-CROWN"
let has_vnnlib_support = function
| Pyrat -> true
- | Marabou | Saver | Aimos | CVC5 | Nnenum -> false
+ | Marabou | Saver | Aimos | CVC5 | Nnenum | ABCrown -> false
diff --git a/src/prover.mli b/src/prover.mli
index 38b02037e6cbda8b97e9593f59fa0968babad78f..b993523e327e11a5e418db531f159e647a0829e4 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -27,6 +27,7 @@ type t = private
| Aimos [@name "AIMOS"]
| CVC5 [@name "cvc5"]
| Nnenum [@name "nnenum"]
+ | ABCrown [@name "alpha-beta-CROWN"]
[@@deriving yojson, show]
val list_available : unit -> t list
diff --git a/src/verification.ml b/src/verification.ml
index 8488a8742715fad4844811df1d2c2511ce98ecfb..860a96948eb65f5e6d80636e1a57e212cee6c3b7 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -262,7 +262,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
| (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
let dataset = Unix.realpath (Option.value_exn dataset) in
answer_dataset limit config env prover config_prover driver dataset task
- | Marabou | Pyrat | Nnenum ->
+ | Marabou | Pyrat | Nnenum | ABCrown ->
let task = Interpretation.interpret_task ~cwd env task in
let proof_strategy = Proof_strategy.apply_native_nn_prover in
answer_generic limit config env prover config_prover driver