[SMT-LIB] New logic for SMTLIBv2 - Separation Logic

[Viktor Kuncak]

Dear Mihaela and Martin

Thank you for the comments. The discussion on separation logic is very
interesting because it brings another view to problems for which
otherwise one would normally use array theories, possibly with
quantifiers. Postponing for the moment the issues of the SL-SMT
marriage arrangements, let me just note two somewhat orthogonal
points.

Regarding this point:

"3. A paper giving the semantics of the theory has been written and is
currently under submission to FMCAD."

If the content of this report is to be used as an argument for
community discussion, it should probably be made available as a
technical report. This would not interfere in any way with the FMCAD
reviewing process (in case this is still relevant).

Regarding this point:

"by the five competing solvers includes mutually recursive functions
(used to specify inductive definitions of data structures) which are
prohibited by the current version of SMT-LIB Standard (page 59)."

I believe that this restriction should be lifted. The first-order
spirit of SMT-LIB is preserved if we preserve the current translation
of

define-fun f (x) t

into

forall (x) (f x) = t

In particular, unfolding of recursive definitions is sound with
respect to such first-order axiom. I also see no problem with any
Inconsistencies that may be introduced by the resulting universal
axiom. One just needs to keep in mind that define-fun, like
assumptions, may introduce inconsistency.

Best regards
  Viktor

On Mon, May 26, 2014 at 10:14 PM, Mihaela Sighireanu
<sighirea at liafa.univ-paris-diderot.fr> wrote:
> Dear Cesare and David,
>
>
>
>>> Before we see the details of the proposal by the SL community of an
>>> SMT-LIB theory modeling separation logic, I would recommend that SMT-COMP
>>> organizers clearly distinguish this new demonstration division from the rest
>>> of SMT-COMP and in fact even call it something else, like SL-COMP, say.
>>
>> Will do.
>
>
> I've posted your recommendation on the discussion list of our group and
> there is not objection to have a different naming for our division.
>
> Moreover, Cesare's remark makes perfect sense because the SL fragment dealt
> by the five competing solvers includes mutually recursive functions (used to
> specify inductive definitions of data structures) which are prohibited by
> the current version of SMT-LIB Standard (page 59).
>
> However, I found very interesting the following comment of David:
>
>> ..., there is sufficient cross-fertilization that I would
>>
>> like to see close ties between classic SMT-LIB and any SL logics. For
>> example, SMT solvers that handle SL logic might well want to be
>> extended to also support other logics already present in SMT-LIB.
>> Having the SMT-LIB benchmarks and the results of other solvers
>> available would be a significant benefit. Incorporating the same basic
>> abstract and concrete syntax, with just a few extensions for SL that
>> are non-classic-SMTLIB would help with the goal of unifying the
>> discussion and research work of two now somewhat separate research
>> communities.
>
>
> and, to support this comment, I would like to give you two references to
> very recent works:
>
> Juan Antonio Navarro Pérez, Andrey Rybalchenko: Separation Logic Modulo
> Theories. APLAS 2013
>
> Ruzica Piskac, Thomas Wies, Damien Zufferey: Automating Separation Logic
> Using SMT. CAV 2013
>
>
>
>>> So the next step in this instance is for the SMT-LIB coordinators to have
>>> a
>>> round of emails with Mihaela, and whoever else she would like to include,
>>> to see if the conditions to move to Step 2 are satisfied.
>
>
> Although the pre-condition 1a) listed by Cesare is not satisfied by our SL
> fragment, I've posted on our discussion group  a call for volunteers to
> build such a group. Please inform me if forming an SL-SMTLIB group makes
> sense.
>
> Best regards,
> Mihaela
>
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib



-- 
Viktor Kuncak
http://lara.epfl.ch/~kuncak