# Changeset 3431 for Papers/fopara2013/fopara13.tex

Ignore:
Timestamp:
Feb 14, 2014, 12:09:26 PM (6 years ago)
Message:

Note the specification language in Sec 3.

File:
1 edited

### Legend:

Unmodified
 r3430 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 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 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.