diff --git a/README.md b/README.md
index ece96bd1fcb382b6295080840e80b467b95e39b2..e717232f94e584ab011f6e98f4f134262a9414c9 100644
--- a/README.md
+++ b/README.md
@@ -1,36 +1,23 @@
 # Residual Runtime Verification via Reachability Analysis
 
-## Implementation Details
+## Implementation details
 
 The work is implemented as a plugin (1 KLOC) to the [BISM](https://gitlab.inria.fr/bism/bism-public) Java byte-code instrumentation tool.
-%
 BISM is a lightweight instrumentation tool that features an expressive and high-level instrumentation language. 
-%
 Instrumentation directives in BISM are given with the so-called transformers, which resemble aspects of aspect-oriented programming.
-%
 Writing static analyzers requires a fine level of granularity when capturing program events.
-%
 The BISM instrumentation language provides access to the level of bytecode instructions with full static and dynamic context objects.
-%
 It is also control-flow aware.
-%
 That is, it generates CFGs for all methods and provides access to them in its language. %
-%
 Both features are essential for our residual analysis; this makes BISM the instrumentation framework of choice for our purposes. 
  
-%
 Moreover, BISM provides a mechanism to compose multiple transformers.
-%
 Transformers, in composition, are capable of controlling the visibility of instructions.
-%
 For each property, we then write two transformers: the first one, the static analyzer, that performs the residual analysis and hides safe instructions, and the second one is to instrument the residual part of the program for runtime monitoring.
-%
 We extend BISM with a module that provides automata operations.
-%
-The module is used to generate the CFG automata of methods and prepare the automaton for bad prefixes, as described in Sections~\ref{sec:capturingbehaviour} and \ref{sec:BadPrefixAutomaton}.
-%
-The module also allows us to detect the property-violating execution paths, as described in Section~\ref{sec:findingviolations}, by intersecting the language of the CFG automata with the language of bad/good prefixes of the property under consideration.
-%
+The module is used to generate the CFG automata of methods and prepare the automaton for bad prefixes.
+The module also allows us to detect the property-violating execution paths by intersecting the language of the CFG automata with the language of bad/good prefixes of the property under consideration.
+
 
 
 ## To run the tool