Spell check.

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -510,7 +510,7 @@ digraph ast {
 }
 \enddot
 
-In the CPROVER framework, we provide a precise implemenation of Φ, using explicitly tracked
+In the CPROVER framework, we provide a precise implementation 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 CPROVER, versus a Φ-based approach in
@@ -701,7 +701,7 @@ to prove that the factorial function never returns 0.
 An abstract interpretation is made up from four ingredients:
 1. An **abstract domain**, which represents the analysis results.
 2. A family of **transformers**, which describe how basic programming
-   languge constructs modify the state.
+   language constructs modify the state.
 3. A way to map from pairs of program locations (e.g., positions in the
    program code) and variable names to values in the abstract domain.
 4. An algorithm to compute a ''fixed point'', computing a map as described
@@ -877,7 +877,7 @@ topics can be found in the literature as well.
 
 \section Glossary_section Glossary
 
-\subsectino instrument_subsection Instrument
+\subsection instrument_subsection Instrument
 
 To instrument a piece of code means to modify it by (usually) inserting new
 fragments of code that, when executed, tell us something useful about the code