Restructure ReadMe and complete the "quick start" steps

Author: karoliineh

README.md

@@ -1,36 +1,57 @@
-# sv-comp-witness-vscode
+# sv-comp-witness-VS Code
 
-Integration of [SV-Comp](https://sv-comp.sosy-lab.org/) verification tools for C into VS Code
-for visualizing their combined verification witnesses.
+VS Code extension for running [SV-COMP](https://sv-comp.sosy-lab.org/) verification tools and
+visualizing their witnesses (correctness witnesses / invariants) for C programs.  
+Runs one or more verifiers via **fm-weck** and renders their invariants inline in the editor.
 
-## Developing
+## Use the extension
+
+### Prerequisites
+- VS Code
+- fm-weck installed and working  
+  (with its own prerequisites, e.g., a container runtime such as Podman)
+
+### Installing
+
+1. Install [fm-weck](https://gitlab.com/sosy-lab/software/fm-weck)
+2. Get the extension package (`.vsix`) by either:
+    * Downloading the extension from [latest GitHub Actions build](https://github.com/sws-lab/sv-comp-witness-vscode/actions) → choose a workflow run → Artifacts → `wiivi-plugin`
+    * Building the extension (see [Building](#building))
+3. Install the extension into VS Code:
+```shell
+cd VS Code && code --install-extension sv-comp-verifiers-0.0.1.vsix
+```
+
+### Quick start
+
+After installing the extension:
+
+1. Open the project in **VS Code** (e.g., calling `code .` in the project root directory).
+2. Open the file `standard_strcpy_original-2.i` in VS Code.
+3. Locate and open the **Witnesses** panel.
+4. In the panel **select** a data model, property, and which tools to run.
+5. Click **Analyze** to start analyzing the currently open file.  
+   (*Note: the first time run will take time with fm-weck getting the required tools.*)
+3. The invariants from the tools should be shown above lines 22, 26, and 31.
+
+## Build / Develop the extension
+
+### Prerequisites
 
 Make sure the following are installed:
 - `JDK 17`
 - `mvn`
 - `npm`
 - `nodejs`
-- `vsce` (using `npm install -g @vscode/vsce` for example)
+- `vsce` (using `npm install -g @VS Code/vsce` for example)
 - [fm-weck](https://gitlab.com/sosy-lab/software/fm-weck)
 
 
+ ### Building
 To build this extension, run the commands starting from project root directory:
 1. `mvn install` (or can use `mvn package -Dmaven.test.skip` if tests are failing)
-2. `cd vscode`
+2. `cd VS Code`
 3. `npm install` (only needed the first time)
 4. `vsce package`
 
-### Installing
 
-Install the extension into VS Code with
-```shell
-cd vscode && code --install-extension sv-comp-verifiers-0.0.1.vsix
-```
-
-## Testing
-
-Note that the first time run will take time with fm-weck getting the required tools.
-
-1. Open the project in VS Code after installing the extension.
-2. Open the file `standard_strcpy_original-2.i` in VS Code.
-3. The combined invariants should be shown above lines 22, 26, and 31.