Skip to content

Commit

Permalink
Fix numbers
Browse files Browse the repository at this point in the history
  • Loading branch information
andreaslindner committed Jul 31, 2024
1 parent 2b6c3ab commit 4ec00ed
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions examples/riscv/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ Proof
QED
```

### 5. BIR symbolic execution analysis
### 7. BIR symbolic execution analysis

- built on a [general theory of symbolic execution](https://arxiv.org/abs/2304.08848) instantiated for BIR
- **automatic** inside HOL4 if parameters have the right shape
Expand All @@ -230,7 +230,7 @@ Proof
QED
```

### 6. Specifying and proving BSPEC contracts using symbolic analysis results
### 8. Specifying and proving BSPEC contracts using symbolic analysis results

- requires manual specification of beginning and end program labels for contract
- **automatic** inside HOL4 if parameters have the right shape
Expand All @@ -248,7 +248,7 @@ Proof
QED
```

### 6. Proving High Level BIR Contract
### 9. Proving High Level BIR Contract

- built on a [general Hoare-style logic](https://doi.org/10.1007/978-3-030-58768-0_11) for unstructured programs
- requires auxiliary results from above steps
Expand All @@ -267,7 +267,7 @@ Proof
QED
```

### 7. Backlifting High Level BIR contract to RISC-V binary
### 10. Backlifting High Level BIR contract to RISC-V binary

- built on a [general Hoare-style logic](https://doi.org/10.1007/978-3-030-58768-0_11) for unstructured programs
- requires collecting auxiliary results from above steps
Expand Down

0 comments on commit 4ec00ed

Please sign in to comment.