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

Mon May 26 00:53:03 EDT 2014

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.

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.

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.

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.

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