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

[Martin Brain]

On Thu, 2014-05-22 at 05:10 -0700, 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;

Is it available online?  I've checked the archive of the groups and the
git repository.  The link on
https://github.com/mihasighi/smtcomp14-sl/wiki currently gives a 404
error.

>  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? 

For floating-point, the procedure was as follows:

1. A draft of the theory was presented at SMT'14

2. A working group of interested parties was formed and discussed
various drafts until a concensus was achieved.

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

HTH

Cheers,
 - Martin