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

[cok at frontiernet.net]

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