From 1d155fadc0bfed2eb814784e2399d2d2e3b5e6c0 Mon Sep 17 00:00:00 2001
From: SOUEIDI Chukri <chukri.a.soueidi@inria.fr>
Date: Thu, 28 Jul 2022 17:28:47 +0000
Subject: [PATCH] Update README.md

---
 README.md | 21 ++++-----------------
 1 file changed, 4 insertions(+), 17 deletions(-)

diff --git a/README.md b/README.md
index ece96bd..e717232 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
-- 
GitLab