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

Mon May 26 08:46:51 EDT 2014

Cesare,

On 5/26/2014 12:53 AM, Tinelli, Cesare wrote:
> David,
>
> It is exciting to see that a new community of separation logic solvers is forming and that the SMT-COMP organizers are willing to have a demonstration division for such solvers at SMT-COMP'14.
>
> 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.
> The reason is that is not clear at the moment that the "QF_S" logic you mention below could be defined a sub-logic of the underlying (classical, first-order) SMT-LIB logic. If that is not possible, we would not be able to incorporate separation logic in the SMT-LIB standard. Hence, it could be confusing to have a separation logic division at SMT-COMP which is a competition of SMT-LIB-compliant solvers.
I welcome more discussion on this point, as I am not an expert in SL 
logics. However, although the SL  theory is expressible in the SMT-LIB 
concrete syntax, I don't believe as it is formulated, it is a sub-logic 
of the underlying SMT-LIB logic. Perhaps it can be reformulated as such 
a sub-logic.

But even if not, 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.
> Also, I would not recommend using QF_S for the logic since we already had plans to use S for the theory of sequences, which is currently under discussion and I hope will be finalized soon.
We'll use QF_S for this trial round, to avoid having to settle the issue 
while participants are finalizing benchmarks and solvers. When there is 
a decision on naming and how SL is to be related to the current SMTLIB, 
we can change the benchmarks. This very question is why I posed the 
discussion question about naming of theories and logics.
>
> As for the process of proposing a new SMT-LIB theory, here are the steps that have been followed in the past:
>
> 1) A person or a group has a first round of discussions with the SMT-LIB coordinators
>     to see if there exist basic conditions for a new SMT-LIB theory and related logics.
>     These conditions include
>     a) The proposed theory can be in fact modeled as an SMT-LIB theory (i.e., as a set
>        of many-sorted structures over a first order signature, as specified in the
>        SMT-LIB standard.)
>     b) There are enough people interested in using this theory.
>     c) There are, or there could be, enough benchmarks based on this theory.
>
> 2) A work group is formed consisting of people interested in the new theory, including
>     solver developers, users, and one or more of the SMT-LIB organizers (the role of the
>     latter is mostly to make sure that the proposed theory and the logic definition are
>     SMT-LIB compliant).
>
> 4) The work group discusses the extension in depth and prepares a detailed proposal.
>
> 5) The proposal is presented to the SMT-LIB community via this discussion list.
>
> 6) Feedback from the community is used to improve the final version of the proposal.
>
> 7) The proposed extension is officially incorporated into the standard and documented on the SMT-LIB site.
>
> 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.
I'll leave that to Mihaela to answer.
> Best,
>
>
> Cesare
>
>
> On 22 May 2014, at 07:10, cok at frontiernet.net wrote:
>
>> Resending compilations of previous notes, this time to smt-lib:
>>
>>  From David Cok:
>>
>> The SMTCOMP organizers have received a request to run, as part of
>> SMTCOMP 2014, a division of solvers that solve separation logic problems
>> expressed in SMTLIBv2, with a logic that incorporates a new theory. We
>> are tentatively expecting 5 solvers to participate. There is a draft
>> theory and logic in development; for now, the logic is named QF_S,
>> though we may decide that a different name is appropriate in the future.
>> Together with Mihaela Sighireanu (copied here, and her email below) and the interested
>> community, we are in the process of curating a set of benchmarks for
>> this division. As far as SMTCOMP is concerned, this is a demonstration
>> division; we will measure and report results as best we can, given the
>> provisional and experimental nature of the benchmarks, theory, logic,
>> and their incorporation into StarExec. A goal is to have this be a
>> full-fledged part of SMTCOMP in future years.
>>
>> I have two questions for the smt-lib community. To separate the
>> discussion, I'll put the second in a separate email.
>>
>> First question: I expect there should be some process for proposing,
>> vetting, commenting, revising new theories and logics. It is a sign of
>> success that such new contributions arise from new quarters, perhaps
>> even previously unknown to SC members. The SL-SMTLIB community that is
>> working on this would appreciate some advice (and encouragement, I'm
>> sure) about how to fold their work into SMT-LIB as a whole. How should
>> we proceed beyond proposals?
>>
>>
>> --------------
>>
>>  From Mihaela Sighireanu:
>>
>> Thank you David for this introduction of our group in the SMT-COMP
>> community.
>>
>> I'm pleased to inform the [SMTLIB community] about the process used
>> inside the Separation Logic (SL) group (called SL-SMTCOMP by David) in
>> order to fix the theory and the benchmark for this trial at the
>> SMT-COMP'14 edition.
>>
>> A first version of the theory and of the benchmark has been proposed to
>> a list of 8 groups (18 persons) which have published works on SL solvers
>> (for satisfiability or entailment checking problems).
>> The idea of participating at this edition of SMT-COMP has been approved
>> by a majority of these groups (5). Three other groups have expressed
>> their interest for having such a theory developed and the preference to
>> postpone their participation for the 2014 competition.
>> In this preliminary step, I've received proposals to add two more groups
>> to the list of discussion.
>>
>> A list of discussion has been created as a Google group:
>>
>> https://groups.google.com/forum/#!forum/smtcomp14-sl
>>
>> This list includes the peoples from the 10 groups (22 persons).
>> David has been added at the discussion group.
>>
>> To ease the work on the benchmark, we have created a GitHub project
>> which provides the theory definition, the benchmarks, and a wiki:
>>
>> https://github.com/mihasighi/smtcomp14-sl
>>
>> The GitHub archive includes also a tool for compiling the SMTLIB v2
>> format to the internal format of the participating solvers.
>>
>> At the present time, the version of the theory is almost fixed.
>> The discussions concern the semantics of the user defined predicates
>> built on the top of this theory.
>> We hope to reach a consensus soon (this week) and to update the
>> benchmark accordingly.
>>
>> For the next editions, we expect to add new classes of examples and
>> problems (e.g., verification conditions, combination of SL with other
>> theories).
>>
>>
>> The SL-SMTLIB community that is
>>> working on this would appreciate some advice (and encouragement, I'm
>>> sure) about how to fold their work into SMT-LIB as a whole.
>>>
>> Indeed, the comments and advices of the SMT SC and the working groups of
>> SMT would be very useful for us.
>>
>> Best regards,
>>
>> -- 
>> Mihaela Sighireanu
>> -- 
>> University Paris Diderot - Paris 7
>> Laboratory LIAFA,
>> Building Sophie Germain, case 7014,
>> 4th floor, room 426,
>> 75205 Paris Cedex 13
>> Phone: +33 1 57 27 54 19
>> Web: www.liafa.univ-paris-diderot.fr/~sighirea
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib