The CAISAR Platform¶

The CAISAR logo
Authors:

Michele Alberti, François Bobot, Julien Girard, Alban Grastien

Version:

3.0, January 2025

Copyright:

2020–2025 CEA (Commissariat à l’énergie atomique et aux énergies alternatives)

This work has been partly supported by the Confiance.ai program and the DeepGreen project.

  • 1. Foreword
    • 1.1. Overall Design
    • 1.2. Availability
    • 1.3. Contact
    • 1.4. Acknowledgements
  • 2. Installation
    • 2.1. Install through Opam
    • 2.2. Install through Docker
    • 2.3. Install through Nix
    • 2.4. Compile from source
  • 3. Using CAISAR
    • 3.1. Commands summary
    • 3.2. Command line options
    • 3.3. Prover registration
    • 3.4. Property verification
    • 3.5. Built-in properties
    • 3.6. Advanced usage: registering a new prover
  • 4. CAISAR by Examples
    • 4.1. Functional properties of ACAS-Xu
    • 4.2. (Local) Robustness of MNIST dataset
    • 4.3. Verification of Support Vector Machines
  • 5. The CAISAR modelling language
    • 5.1. Origin: WhyML
    • 5.2. Built-ins
  • 6. Hacking CAISAR
    • 6.1. CAISAR project structure
    • 6.2. Setting up a development environment
    • 6.3. Opening a merge request
  • 7. Supported provers
    • 7.1. PyRAT
    • 7.2. Marabou
    • 7.3. SAVer
    • 7.4. nnenum
    • 7.5. alpha-beta-CROWN
    • 7.6. SMT solvers
  • Index
  • CAISAR website

CAISAR

Navigation

  • 1. Foreword
  • 2. Installation
  • 3. Using CAISAR
  • 4. CAISAR by Examples
  • 5. The CAISAR modelling language
  • 6. Hacking CAISAR
  • 7. Supported provers
  • Index
  • CAISAR website

Related Topics

  • Documentation overview
    • Next: 1. Foreword

Quick search

©1980, The CAISAR Development Team. | Powered by Sphinx 7.4.7 & Alabaster 0.7.16 | Page source