Spell checking

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -331,7 +331,7 @@ digraph ast {
 
 Note that the parameter `n` in `factorial` and the local variable `n` in
 `main` are now disambiguated as `n.1` and `n.2`; furthermore, we leave
-the names of global objects as-is. In the CProver framework, a more
+the names of global objects as-is. In the CPROVER framework, a more
 elaborate system is used: local variables are prefixed with the function names,
 and further disambiguation is performed by adding indices. For brevity,
 we use indices only.
@@ -463,7 +463,7 @@ This function consists of four basic blocks:
 4. `return fac.1`
    (this block has a label, `for_loop_end`).
 
-One way to undestand which functions form basic blocks is to consider the
+One way to understand which functions form basic blocks is to consider the
 successors of each instruction. If we have two instructions A and B, we say
 that B is a *successor* of A if, after executing A, we can execute B without any
 intervening instructions. For instance, in the example above, the loop
@@ -472,11 +472,11 @@ initialization statement `unsigned long int i.1 = 1` is a successor of
 of `unsigned long fac.1 = 1`: we always have to execute some other intermediate
 statements to reach the return statement.
 
-Now, consider the `if` statment,
+Now, consider the `if` statement,
 `if (i.1 <= n.1) goto for_loop_entry else goto for_loop_end`.
 This statement has *two* successors: `fac.1 *= i.1` and `return fac.1`.
 
-Similarily, we say that A is a *predecessor* of B if B is a sucessor of A.
+Similarly, we say that A is a *predecessor* of B if B is a successor of A.
 We find that the `if` statement has two predecessors,
 `unsigned int i.1 = 1` and `goto for_loop_start`.