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

[Mihaela Sighireanu]

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