Index: /Papers/fopara2013/fopara13.bib
===================================================================
--- /Papers/fopara2013/fopara13.bib (revision 3430)
+++ /Papers/fopara2013/fopara13.bib (revision 3431)
@@ -263,2 +263,17 @@
bibsource = {DBLP, http://dblp.uni-trier.de}
}
+
+@inproceedings{bobot,
+ year={2012},
+ isbn={978-3-642-34280-6},
+ booktitle={Formal Methods and Software Engineering},
+ volume={7635},
+ series={Lecture Notes in Computer Science},
+ editor={Aoki, Toshiaki and Taguchi, Kenji},
+ doi={10.1007/978-3-642-34281-3_14},
+ title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
+ url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
+ publisher={Springer Berlin Heidelberg},
+ author={Bobot, FranÃ§ois and FilliÃ¢tre, Jean-Christophe},
+ pages={167-181}
+}
Index: /Papers/fopara2013/fopara13.tex
===================================================================
--- /Papers/fopara2013/fopara13.tex (revision 3430)
+++ /Papers/fopara2013/fopara13.tex (revision 3431)
@@ -79,5 +79,5 @@
Bologna \and
LFCS, School of Informatics, University of Edinburgh
-\and INRIA (Team $\pi$r2 )
+\and INRIA (Team $\pi r^2$)
\and
Universit\`e Paris Diderot
@@ -461,5 +461,6 @@
simple automatic synthesiser for complexity assertions which can
be overridden by the user to increase or decrease accuracy. These are the blue
-comments starting with \lstinline'/*@' in \autoref{itest1}. From the
+comments starting with \lstinline'/*@' in \autoref{itest1}, written in
+Frama-C's specification language, ACSL. From the
assertions, a general purpose deductive platform produces proof
obligations which in turn can be closed by automatic or interactive
@@ -1050,10 +1051,10 @@
such as linked lists, trees, or graphs, the use of traditional first-order logic
to specify, and of SMT solvers to verify, shows some limitations. Separation
-logic~\cite{separation} is an elegant alternative. It is a program logic
+logic is an elegant alternative. It is a program logic
with a new notion of conjunction to express spatial heap separation. Bobot has
recently introduced automatically generated separation
predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition
generator, and the theorem provers were not designed with separation logic in
-mind. CerCo's plugin can exploit the separation predicates to automatically
+mind~\cite{bobot}. CerCo's plugin can exploit the separation predicates to automatically
reason on the cost of execution of simple heap manipulation programs such as an
in-place list reversal.