Commit 2c6d59cf authored by Benoit Viguier's avatar Benoit Viguier
Browse files

typo

parent 5f278c87
......@@ -224,7 +224,7 @@ what these tools carry out conceptually.
\begin{answer}{EEEEEE}
SMT solvers strategies are in need of annotation, often written
as parable comment in the middle of the C code~\cite{acsl}
as parsable comment in the middle of the C code~\cite{acsl}
in order to ``guide'' the proof. In our case we only need to
annotate the beginning of the function and loop invariants
which allows us to get tighter bounds.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment