diff --git a/subprojects/cfa/README.md b/subprojects/cfa/README.md
index a6aba8f3e0..372b40e108 100644
--- a/subprojects/cfa/README.md
+++ b/subprojects/cfa/README.md
@@ -31,7 +31,7 @@ After performing the havoc, `v` is assigned a non-deterministic value.
 This can be used to simulate non-deterministic input from the user or the environment.
 
 Algorithms are usually interested in proving that the error location (given in the CFA or as a separate argument) is not reachable.
-For more information see Section 2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf).
+For more information see Section 2 of the [Software Verification Supplementary Material](https://ftsrg.mit.bme.hu/software-verification-notes/software-verification.pdf), which also includes examples on how to encode programs as CFA.
 
 Variables of the CFA can have the following types.
 * `bool`: Booleans.
@@ -54,8 +54,16 @@ Expressions of the CFA include the following.
 
 ### Textual representation (DSL)
 
-An example CFA realizing a counter:
+As an example, consider a simple program (written in a C-like language) that counts up to 5 and asserts the result to be less than or equal to 5:
+```c
+int x = 0;
+while (x < 5) {
+  x++;
+}
+assert x <= 5;
+```
 
+The program above can be represented by the following CFA:
 ```
 main process counter {
     var x : int
@@ -75,6 +83,8 @@ main process counter {
     L3 -> ERR { assume not (x <= 5) }
 }
 ```
+Note that for example the loop in the program appears as a cycle (`L1 -> L2 -> L1`) in the CFA.
+The assertion is modeled with a branching in the CFA: if it holds, `L3 -> END` is taken, otherwise `L3 -> ERR`.
 
 Variables can be defined by `var <NAME> : <TYPE>`, locations by `(init|final|error|) loc <NAME>`, and edges by `<SOURCE> -> <TARGET> {<STATEMENT>}`.
 Note that it is also possible to include multiple statements on one edge (in new lines).