[userman] proof read overview update

doc/userman/user-overview.tex

@@ -11,7 +11,7 @@ other analyzers in the framework. Thanks to this approach, \FramaC can provide
 a number of sophisticated tools such as a concurrency safety analysis
 (Mthread~\cite{mthread}),
 an enforcer of secure information flow (SecureFlow~\cite{secureflow1,secureflow2}),
-or a coverage-based test generator (LTest~\cite{ltest}), among many others.
+or a set of tools for various test coverage criteria (LTest~\cite{ltest}), among many others.
 
 \section{\FramaC as a Code Analysis Tool}
 
@@ -110,9 +110,9 @@ review.
 \section{\FramaC as a Tool for \C programs}
 
 The \C source code analyzed by \FramaC is assumed to follow the \tool{C99} ISO
-standard\index{C99 ISO standard@\tool{C99} ISO standard}\footnote{Some common
-GCC extensions, as well as some parts of the \tool{C11} standard, are
-also supported.}. \C comments may
+standard\index{C99 ISO standard@\tool{C99} ISO standard}\footnote{Some parts of
+the \tool{C11} standard, as well as some common GCC extensions,
+are also supported.}. \C comments may
 contain \acsl annotations~\cite{acsl} used as specifications to be interpreted
 by \FramaC. The subset of \acsl currently interpreted in \FramaC is described
 in~\cite{acsl-implem}.
@@ -141,7 +141,7 @@ documentation~\cite{value,wp,eacsl}.
 Additional plug-ins can be provided by third-party developers and installed
 separately from the kernel. \FramaC is thus not limited to the set of analyses
 initially installed. For instance, it may be extended with the \tool{Frama-Clang}
-plug-in~\cite{framaclang}, which provides a front-end for C++ code;
+plug-in~\cite{framaclang}, which provides an experimental front-end for C++ code;
 or \tool{MetAcsl}~\cite{metacsl}, which allows specifying higher-level
 meta-properties; among others.
 

doc/userman/userman.bib

@@ -127,18 +127,17 @@ note={Extended version of \cite{sefm12}},
   school = {Universit\'e Rennes 1},
 }
 
-@article{ltest,
-  TITLE = {{Detection of Polluting Test Objectives for Dataflow Criteria}},
-  AUTHOR = {Martin, Thibault and Kosmatov, Nikolai and Pr{\'e}vosto, Virgile and Lemerre, Matthieu},
-  URL = {https://hal-cea.archives-ouvertes.fr/cea-02974228},
-  NOTE = {International Conference on Integrated Formal Methods 2020-11-16/20, Lugano, Suisse},
-  JOURNAL = {{Lecture Notes in Computer Science}},
-  PUBLISHER = {{Springer}},
-  NUMBER = {12546},
-  YEAR = {2020},
-  PDF = {https://hal-cea.archives-ouvertes.fr/cea-02974228/file/main.pdf},
-  HAL_ID = {cea-02974228},
-  HAL_VERSION = {v1},
+@inproceedings{ltest,
+  author    = {Micha{\"{e}}l Marcozzi and
+               S{\'{e}}bastien Bardin and
+               Micka{\"{e}}l Delahaye and
+               Nikolai Kosmatov and
+               Virgile Prevosto},
+  title     = {Taming Coverage Criteria Heterogeneity with LTest},
+  booktitle = {2017 {IEEE} International Conference on Software Testing, Verification
+               and Validation, {ICST} 2017, Tokyo, Japan, March 13-17, 2017},
+  pages     = {500--507},
+  year      = {2017},
 }
 
 @manual{mthread,