diff --git a/.github/actions/build-archive/README.md b/.github/actions/build-archive/README.md
index 7531f3573a..9aa53f4212 100644
--- a/.github/actions/build-archive/README.md
+++ b/.github/actions/build-archive/README.md
@@ -24,8 +24,8 @@ Minimal necessary packages for Ubuntu 22.04 LTS:
 ├── lib - contains the native library dependencies
 ├── offset.sh - creates a mapping between statements of two C files
 ├── solvers - contains further dependencies (SMT-solvers), each having their respective licenses 
-├── specification-transformation.bin - binary for transforming various specifications to reachability
-├── specification-transformation.bin.LICENSE - license for `specification-transformation.bin`
+├── specification-transformation - binaries for transforming various specifications to reachability (this includes cpachecker, but we do not use it for verification.)
+├── specification-transformation.LICENSE - license for `specification-transformation`
 ├── theta-smtlib.jar - the jarfile for installing and managing smt solvers (not necessary unless different solver versions are required)
 ├── theta-start.sh - the starting script of TOOL_NAME
 └── theta.jar - the main jarfile of TOOL_NAME
diff --git a/.github/actions/build-archive/action.yml b/.github/actions/build-archive/action.yml
index 88b78332d3..2238396805 100644
--- a/.github/actions/build-archive/action.yml
+++ b/.github/actions/build-archive/action.yml
@@ -58,16 +58,14 @@ runs:
       with:
         name: specification-transformation
         path: ./
-    - name: Move file to overwrite specification-transformation.bin
-      shell: bash
-      run: |
-        mv specification-transformation.bin $GITHUB_ACTION_PATH/specification-transformation.bin
     - name: Copy specification transformation binary and license
       shell: bash
       run: |
-        cp $GITHUB_ACTION_PATH/specification-transformation.bin ${{ inputs.name }}/${{ inputs.name }}/
-        chmod +x ${{ inputs.name }}/${{ inputs.name }}/specification-transformation.bin
-        cp $GITHUB_ACTION_PATH/specification-transformation.bin.LICENSE ${{ inputs.name }}/${{ inputs.name }}/
+        zipfile=$(realpath ./specification-transformation.zip)
+        pushd ${{ inputs.name }}/${{ inputs.name }}/
+        unzip $zipfile
+        popd
+        cp $GITHUB_ACTION_PATH/specification-transformation.LICENSE ${{ inputs.name }}/${{ inputs.name }}/
         cp $GITHUB_ACTION_PATH/offset.sh ${{ inputs.name }}/${{ inputs.name }}/
     - name: ZIP archive
       shell: bash
diff --git a/.github/actions/build-archive/specification-transformation.bin.LICENSE b/.github/actions/build-archive/specification-transformation.LICENSE
similarity index 100%
rename from .github/actions/build-archive/specification-transformation.bin.LICENSE
rename to .github/actions/build-archive/specification-transformation.LICENSE
diff --git a/.github/actions/build-spec-transformation/action.yml b/.github/actions/build-spec-transformation/action.yml
index 8a1b13e22b..51511cfd4c 100644
--- a/.github/actions/build-spec-transformation/action.yml
+++ b/.github/actions/build-spec-transformation/action.yml
@@ -7,8 +7,8 @@ runs:
     - name: Print file path
       shell: bash
       run: |
-        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }}
-        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
+        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }}
+        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
     - name: Setup java 17
       if: env.file_exists == 'false'
       uses: actions/setup-java@5ffc13f4174014e2d4d4572b3d74c3fa61aeb2c2 # v3.11.0
@@ -37,25 +37,19 @@ runs:
         mv lib/cpachecker/lib/java/runtime/*.jar cpachecker/runtime/
         mv lib/cpachecker/config cpachecker/
         mv lib/cpachecker/cpachecker.jar cpachecker/
-    - name: Install nuitka
+    - name: zip file
       if: env.file_exists == 'false'
       shell: bash
       run: |
-        sudo apt update && sudo apt -y --no-install-recommends install nuitka libfuse2
-    - name: Run nuitka
-      if: env.file_exists == 'false'
-      shell: bash
-      run: |
-        cd specification-transformation
-        bash -c "yes yes || true" | nuitka3 --onefile --standalone --include-data-dir="cpachecker=cpachecker" src/specification-transformation.py 
+        zip specification-transformation.zip specification-transformation/cpachecker specification-transformation/src -r
     - name: Move if exists
       if: env.file_exists == 'true'
       shell: bash
       run: |
         mkdir specification-transformation
-        mv $GITHUB_ACTION_PATH/specification-transformation.bin specification-transformation/
+        mv $GITHUB_ACTION_PATH/specification-transformation.zip ./
     - name: Upload results
       uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:
         name: specification-transformation
-        path: specification-transformation/specification-transformation.bin
+        path: specification-transformation.zip
diff --git a/.github/actions/build-spec-transformation/specification-transformation.bin b/.github/actions/build-spec-transformation/specification-transformation.bin
deleted file mode 100755
index 2a626c001b..0000000000
Binary files a/.github/actions/build-spec-transformation/specification-transformation.bin and /dev/null differ
diff --git a/.github/actions/install-llvm/action.yml b/.github/actions/install-llvm/action.yml
index cf7a29c81f..f9f621537e 100644
--- a/.github/actions/install-llvm/action.yml
+++ b/.github/actions/install-llvm/action.yml
@@ -11,15 +11,15 @@ runs:
       run: |
         # wget https://apt.llvm.org/llvm.sh
         # chmod +x llvm.sh
-        sudo $GITHUB_ACTION_PATH/llvm.sh ${{ inputs.version }}        
+        # sudo $GITHUB_ACTION_PATH/llvm.sh ${{ inputs.version }}        
 
-        sudo ln -sf $(which clang-${{inputs.version}}) /usr/bin/clang
-        sudo ln -sf $(which llvm-config-${{inputs.version}}) /usr/bin/llvm-config
+        # sudo ln -sf $(which clang-${{inputs.version}}) /usr/bin/clang
+        # sudo ln -sf $(which llvm-config-${{inputs.version}}) /usr/bin/llvm-config
 
     - name: Test version
       shell: bash
       run: |
-        ls -l $(which clang)
-        ls -l $(which llvm-config)
-        clang --version
-        llvm-config --version
\ No newline at end of file
+        # ls -l $(which clang)
+        # ls -l $(which llvm-config)
+        # clang --version
+        # llvm-config --version
\ No newline at end of file
diff --git a/.github/actions/install-llvm/llvm.sh b/.github/actions/install-llvm/llvm.sh
index 685f96f939..c2e26ec626 100755
--- a/.github/actions/install-llvm/llvm.sh
+++ b/.github/actions/install-llvm/llvm.sh
@@ -20,7 +20,7 @@ usage() {
     exit 1;
 }
 
-CURRENT_LLVM_STABLE=16
+CURRENT_LLVM_STABLE=18
 BASE_URL="http://apt.llvm.org"
 
 # Check for required tools
@@ -125,7 +125,10 @@ LLVM_VERSION_PATTERNS[13]="-13"
 LLVM_VERSION_PATTERNS[14]="-14"
 LLVM_VERSION_PATTERNS[15]="-15"
 LLVM_VERSION_PATTERNS[16]="-16"
-LLVM_VERSION_PATTERNS[17]=""
+LLVM_VERSION_PATTERNS[17]="-17"
+LLVM_VERSION_PATTERNS[18]="-18"
+LLVM_VERSION_PATTERNS[19]="-19"
+LLVM_VERSION_PATTERNS[20]=""
 
 if [ ! ${LLVM_VERSION_PATTERNS[$LLVM_VERSION]+_} ]; then
     echo "This script does not support LLVM version $LLVM_VERSION"
@@ -161,9 +164,15 @@ if [[ -z "`apt-key list 2> /dev/null | grep -i llvm`" ]]; then
     # Delete the key in the old format
     apt-key del AF4F7421
 fi
-add-apt-repository "${REPO_NAME}"
+if [[ "${VERSION_CODENAME}" == "bookworm" ]]; then
+    # add it twice to workaround:
+    # https://github.com/llvm/llvm-project/issues/62475
+    add-apt-repository -y "${REPO_NAME}"
+fi
+
+add-apt-repository -y "${REPO_NAME}"
 apt-get update
-PKG="clang-$LLVM_VERSION" # lldb-$LLVM_VERSION lld-$LLVM_VERSION clangd-$LLVM_VERSION"
+PKG="clang-$LLVM_VERSION lldb-$LLVM_VERSION lld-$LLVM_VERSION clangd-$LLVM_VERSION"
 if [[ $ALL -eq 1 ]]; then
     # same as in test-install.sh
     # No worries if we have dups
diff --git a/.github/workflows/check-copyright.yml b/.github/workflows/check-copyright.yml
index 7eb1f23215..5f263bbe7c 100644
--- a/.github/workflows/check-copyright.yml
+++ b/.github/workflows/check-copyright.yml
@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-copyright:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
diff --git a/.github/workflows/check-formatting.yml b/.github/workflows/check-formatting.yml
index 02647f3a04..253ed2884e 100644
--- a/.github/workflows/check-formatting.yml
+++ b/.github/workflows/check-formatting.yml
@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-formatting:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
diff --git a/.github/workflows/check-version.yml b/.github/workflows/check-version.yml
index 83cbf94600..f5721f124a 100644
--- a/.github/workflows/check-version.yml
+++ b/.github/workflows/check-version.yml
@@ -9,7 +9,7 @@ concurrency:
 
 jobs:
   check-version:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml
index ab5526956b..a32c8abca5 100644
--- a/.github/workflows/linux-build-test-deploy.yml
+++ b/.github/workflows/linux-build-test-deploy.yml
@@ -18,7 +18,7 @@ concurrency:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -64,7 +64,7 @@ jobs:
             portfolio: BOUNDED
           - tool: Thorn_SV-COMP
             portfolio: HORN
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: create-archives
     steps:
       - name: Checkout repository
@@ -78,7 +78,7 @@ jobs:
   
   collect-results:
     needs: test-benchexec
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -86,7 +86,7 @@ jobs:
         uses: ./.github/actions/benchexec-report
 
   create-spec-transformation:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -94,7 +94,7 @@ jobs:
         uses: ./.github/actions/build-spec-transformation
 
   create-archives:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: [build, create-spec-transformation]
     strategy:
       matrix:
@@ -118,7 +118,7 @@ jobs:
 
   javadoc:
     needs: build
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -129,7 +129,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest]
+        os: [ubuntu-24.04]
     needs: build
     runs-on: ${{ matrix.os }}
     steps:
@@ -142,7 +142,7 @@ jobs:
       - name: Run tests
         uses: ./.github/actions/test-action
       - name: Positive outcome badge
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
@@ -150,7 +150,7 @@ jobs:
           color: "green"
           path: "badges/test-${{ runner.os }}"
       - name: Negative outcome badge
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
@@ -162,7 +162,7 @@ jobs:
   deploy-release:
     needs: [test-linux, create-archives]
     if: "${{ github.event.inputs.message != '' &&  github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -177,7 +177,7 @@ jobs:
   deploy-maven:
     # needs: test-linux
     if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -194,7 +194,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -231,7 +231,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -269,7 +269,7 @@ jobs:
           repository: ftsrg/${{ matrix.dockerprojects }}
 
   deploy-docs:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
diff --git a/.github/workflows/reformat-code.yml b/.github/workflows/reformat-code.yml
index 29411d1f37..29954ac429 100644
--- a/.github/workflows/reformat-code.yml
+++ b/.github/workflows/reformat-code.yml
@@ -10,7 +10,7 @@ on:
 
 jobs:
   reformat:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92
       id: generate-token
diff --git a/.github/workflows/sonar.yml b/.github/workflows/sonar.yml
index c66a14c329..fe8b634a11 100644
--- a/.github/workflows/sonar.yml
+++ b/.github/workflows/sonar.yml
@@ -13,7 +13,7 @@ concurrency:
 
 jobs:
   run-sonar:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
diff --git a/.github/workflows/version-bump.yml b/.github/workflows/version-bump.yml
index d443d1823e..857a64c4fb 100644
--- a/.github/workflows/version-bump.yml
+++ b/.github/workflows/version-bump.yml
@@ -15,7 +15,7 @@ on:
 
 jobs:
   version-bump:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - name: Set java home to java 17
       run: |
diff --git a/build.gradle.kts b/build.gradle.kts
index c3b28cbddc..19d6102585 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.2"
+    version = "6.8.3"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
index 5f5156c2ca..b54acf3c63 100755
--- a/scripts/theta-start.sh
+++ b/scripts/theta-start.sh
@@ -43,13 +43,13 @@ else
     if [ "$(basename "$property")" == "termination.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     else