Changeset 3431

Feb 14, 2014, 12:09:26 PM (8 years ago)

Note the specification language in Sec 3.

2 edited


  • Papers/fopara2013/fopara13.bib

    r3339 r3431  
    263263  bibsource = {DBLP,}
     267  year={2012},
     268  isbn={978-3-642-34280-6},
     269  booktitle={Formal Methods and Software Engineering},
     270  volume={7635},
     271  series={Lecture Notes in Computer Science},
     272  editor={Aoki, Toshiaki and Taguchi, Kenji},
     273  doi={10.1007/978-3-642-34281-3_14},
     274  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
     275  url={},
     276  publisher={Springer Berlin Heidelberg},
     277  author={Bobot, François and Filliâtre, Jean-Christophe},
     278  pages={167-181}
  • Papers/fopara2013/fopara13.tex

    r3430 r3431  
    7979Bologna \and
    8080LFCS, School of Informatics, University of Edinburgh
    81 \and INRIA (Team $\pi$r2 )
     81\and INRIA (Team $\pi r^2$)
    8383Universit\`e Paris Diderot
    461461simple automatic synthesiser for complexity assertions which can
    462462be overridden by the user to increase or decrease accuracy.  These are the blue
    463 comments starting with \lstinline'/*@' in \autoref{itest1}.  From the
     463comments starting with \lstinline'/*@' in \autoref{itest1}, written in
     464Frama-C's specification language, ACSL.  From the
    464465assertions, a general purpose deductive platform produces proof
    465466obligations which in turn can be closed by automatic or interactive
    10501051such as linked lists, trees, or graphs, the use of traditional first-order logic
    10511052to specify, and of SMT solvers to verify, shows some limitations. Separation
    1052 logic~\cite{separation} is an elegant alternative. It is a program logic
     1053logic is an elegant alternative. It is a program logic
    10531054with a new notion of conjunction to express spatial heap separation. Bobot has
    10541055recently introduced automatically generated separation
    10551056predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition
    10561057generator, and the theorem provers were not designed with separation logic in
    1057 mind. CerCo's plugin can exploit the separation predicates to automatically
     1058mind~\cite{bobot}. CerCo's plugin can exploit the separation predicates to automatically
    10581059reason on the cost of execution of simple heap manipulation programs such as an
    10591060in-place list reversal.
Note: See TracChangeset for help on using the changeset viewer.