Data

Tools

Indexes

Applications

Experiments

Open Source Science

imandra-marabou-proof-checking

https://github.com/rdesmartin/imandra-marabou-proof-checking

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (4.8%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Basic Info
  • Host: GitHub
  • Owner: rdesmartin
  • Language: OCaml
  • Default Branch: master
  • Size: 90.2 MB
Statistics
  • Stars: 0
  • Watchers: 2
  • Forks: 1
  • Open Issues: 0
  • Releases: 0
Created almost 3 years ago · Last pushed 11 months ago
Metadata Files
Readme Citation

README.md

Run the proof checker in Imandra

Start Imandra repl:

$ imandra core repl import necessary files ```

use "proof_checker/imports.iml";;

```

Run in program mode

Define the proof you want to use in main_repl.iml then import the file:

ocaml (* in proof_checker/main_repl.iml *) let current_proof = tiny2

```

use "proofchecker/mainrepl.iml";;

```

Run in logic mode

It is currently not possible to run the proof checking algorithm on a specific proof in logic mode(error at the [@@reflect] command). However, it is not important as proof checking should never be conducted in logic mode; we want to reason about the checking algorithm in general, not about checking a specific proof.

Verification

Start Imandra repl:

$ imandra core repl import necessary files ```

use "proof_checker/imports.iml";;

```

Import relevant verification file: ```

use "verification/contradiction_verification.iml";;

```

OCaml extraction

It is possible to extract and run OCaml code using the dune build system:

From the project's root directory: $ dune build ./proof_checker/main_extract.exe $ dune exec -- ./proof_checker/main_extract.exe ./json/tinyJsonProof2.json

Owner

  • Name: Rémi Desmartin
  • Login: rdesmartin
  • Kind: user

Citation (CITATION.cff) 

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
  - family-names: Desmartin, Isac, Passmore, Komendantskaya, Katz
    given-names: Remi, Omri, Grant, Ekaterina, Guy
title: "Imarabou: Proof Checker for DNN Verification"
version: 1.0.0
date-released: 2024-05-09

GitHub Events

Total
  • Watch event: 1
  • Push event: 16
  • Create event: 3
Last Year
  • Watch event: 1
  • Push event: 16
  • Create event: 3