Address some of @hannes-steffenhagen-diffblue's comments.

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -506,9 +506,9 @@ digraph ast {
 }
 \enddot
 
-In CBMC, we use a slightly different solution. For each branch, we keep
-track of which side of the branch was taken, and implement Φ using
-this information. There are also some differences in how loops are
+In CBMC, we provide a precise implemenation of Φ, using explicitly tracked
+information about which branches were taken by the program.
+There are also some differences in how loops are
 handled (finite unrolling in CBMC, versus a Φ-based approach in
 compilers); the CBMC approach will be discussed in a later chapter.
 
@@ -590,7 +590,8 @@ While BMC analyses the program by transforming everything to logic
 formulas and, essentially, running the program on sets of concrete
 states, another approach to learn about a program is based on the idea
 of interpreting an abstract version of the program. This is known
-as **static analysis**, or, more precisely, **abstract interpretation**.
+as **abstract interpretation**. Abstract interpretation is one of the
+main methods in the area of **static analysis**.
 
 The key idea is that instead of looking at concrete program states
 (e.g., ''variable x contains value 1''), we look at some