this repo has no description

[new release] caisar, caisar-xgboost, caisar-ovo, caisar-onnx, caisar-nnet and caisar-ir (0.2)

CHANGES:

- [prover] Integration of the [nnenum](https://github.com/stanleybak/nnenum)
prover.

- [prover] Integration of the
[$\alpha-\beta-$CROWN](https://github.com/stanleybak/nnenum) prover.

- [prover] Integration of the AIMOS metamorphic testing prover.

- [prover] Add printer for VNN-LIB format for property specification as
supported by nnenum and $\alpha-\beta-$CROWN provers.

- [prover] Support for multiple configurations of provers, using the
prover-altern command line option. An example of registering an alternate
configuration is available under config/caisar-detection.conf

- [prover] Add transformation to translate ONNX format into SMTLIB format for
allowing SMTLIB2 compliant provers to work on neural networks.

- [doc] The first version of the CAISAR manual is publicly available on our
[website](caisar-platform.com/documentation). It includes detailed
installation instructions, examples on the ACAS-Xu and MNIST local robustness
benchmarks. Those examples use an experimental interpretation language that is
not fully documented yet.

- [deps] Upgraded Why3 to 1.6.0 version.

- Add verify-json command for verifying a robustness property via a JSON
configuration file.

- Add verification of datasets for classification tasks in terms of a specific
CSV format: each line provides the label in 1st column, and data features in
the other columns.

- Add support for memory and time limits.

- Add debug logging options.

Changed files
+289
packages
caisar
caisar.0.2
caisar-ir
caisar-ir.0.2
caisar-nnet
caisar-nnet.0.2
caisar-onnx
caisar-onnx.0.2
caisar-ovo
caisar-ovo.0.2
caisar-xgboost
caisar-xgboost.0.2
+45
packages/caisar-ir/caisar-ir.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis: "CAISAR's intermediate representation"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"base" {>= "v0.14.0"}
+
"ocamlgraph" {>= "1.8.8"}
+
"ppx_inline_test" {>= "0.12.0"}
+
"ppx_deriving" {>= "4.4.1"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"
+43
packages/caisar-nnet/caisar-nnet.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis: "NNet parser for CAISAR"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"base" {>= "v0.14.0"}
+
"csv" {>= "2.4"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"
+46
packages/caisar-onnx/caisar-onnx.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis: "ONNX parser for CAISAR"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"base" {>= "v0.14.0"}
+
"stdio" {>= "v0.14.0"}
+
"ocaml-protoc-plugin" {>= "4.2.0"}
+
"ocplib-endian" {>= "1.0"}
+
"caisar-ir" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"
+43
packages/caisar-ovo/caisar-ovo.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis: "OVO parser for CAISAR"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"base" {>= "v0.14.0"}
+
"csv" {>= "2.4"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"
+46
packages/caisar-xgboost/caisar-xgboost.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis: "XGBOOST parser for CAISAR"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"base" {>= "v0.14.0"}
+
"ocamlgraph" {>= "1.8.8"}
+
"ppx_deriving" {>= "4.4.1"}
+
"ppx_deriving_yojson" {>= "3.6.1"}
+
"csv" {>= "2.4"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"
+66
packages/caisar/caisar.0.2/opam
···
···
+
opam-version: "2.0"
+
synopsis:
+
"A platform for characterizing the safety and robustness of artificial intelligence based software"
+
maintainer: [
+
"LAISER team, Software Safety and Security Laboratory, CEA-List"
+
]
+
authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+
license: "LGPL-2.1-only"
+
homepage: "https://git.frama-c.com/pub/caisar"
+
doc: "https://git.frama-c.com/pub/caisar"
+
bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+
depends: [
+
"dune" {>= "2.9"}
+
"ocaml" {>= "4.13"}
+
"dune-site" {>= "2.9.0"}
+
"piqi" {>= "0.7.6"}
+
"piqilib" {>= "0.6.14"}
+
"zarith" {>= "1.7"}
+
"ocplib-endian" {>= "1.0"}
+
"base" {>= "v0.14.0"}
+
"stdio" {>= "v0.14.0"}
+
"cmdliner" {>= "1.1.1"}
+
"fmt" {>= "0.8.9"}
+
"logs" {>= "0.7.0"}
+
"ppx_deriving" {>= "5.1"}
+
"yojson" {>= "1.7.0"}
+
"menhirLib" {>= "20210310"}
+
"ppx_deriving_yojson" {>= "3.6.1"}
+
"csv" {>= "2.4"}
+
"why3" {>= "1.6.0"}
+
"re" {>= "1.10.4"}
+
"fpath" {>= "0.7.3"}
+
"yaml" {>= "3.1.0"}
+
"caisar-nnet" {= version}
+
"caisar-ovo" {= version}
+
"caisar-onnx" {= version}
+
"caisar-ir" {= version}
+
"caisar-xgboost" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+
url {
+
src:
+
"https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/0.2/caisar-0.2.tbz"
+
checksum: [
+
"sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069"
+
"sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3"
+
]
+
}
+
x-commit-hash: "c056742afad31eed9fdea0f89f8143f0f0cb382e"