Add kmir tool description and CI workflow

.github/workflows/kmir.yml

@@ -0,0 +1,53 @@
+name: KMIR
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/kmir.yml'
+      - 'kmir-proofs/**'
+
+jobs:
+  run-kmir-proofs:
+    name: Run KMIR proofs
+    runs-on: ubuntu-latest
+    env:
+      container_name: "kmir-${{ github.run_id }}"
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - name: Run Challenge 11 Proofs
+        run: |
+          docker run --rm -t \
+            --name ${{ env.container_name }} \
+            -w /home/kmir/workspace \
+            -u $(id -u):$(id -g) \
+            -v $PWD:/home/kmir/workspace \
+            runtimeverificationinc/kmir:ubuntu-jammy-latest \
+            kmir-proofs/0011-floats-ints/run-proofs.sh
+
+  run-kmir-proofs-negative:
+    name: Run KMIR negative proofs
+    runs-on: ubuntu-latest
+    env:
+      container_name: "kmir-neg-${{ github.run_id }}"
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - name: Run Challenge 11 Negative Proofs
+        run: |
+          docker run --rm -t \
+            --name ${{ env.container_name }} \
+            -w /home/kmir/workspace \
+            -u $(id -u):$(id -g) \
+            -v $PWD:/home/kmir/workspace \
+            runtimeverificationinc/kmir:ubuntu-jammy-latest \
+            kmir-proofs/0011-floats-ints/run-proofs.sh --negative

doc/src/SUMMARY.md

@@ -11,6 +11,7 @@
   - [GOTO Transcoder](./tools/goto-transcoder.md)
   - [VeriFast](./tools/verifast.md)
   - [Flux](./tools/flux.md)
+  - [KMIR](./tools/kmir.md)
 
 ---
 

doc/src/tools.md

@@ -14,4 +14,8 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
  | ESBMC (GOTO-Transcoder) | [![ESBMC](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
  | Flux  | [![Flux](https://github.com/model-checking/verify-rust-std/actions/workflows/flux.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/flux.yml)      |
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
+ | KMIR Symbolic Rust Execution | [![KMIR](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml)      |
  | VeriFast for Rust   | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml)      |
+
+
+