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

[Martin Brain]

On Thu, 2014-05-22 at 16:33 +0200, Mihaela Sighireanu wrote:
> Dear Martin,
> 
> > 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.
> 
> Thanks for signaling me this, it was a typo in the link.
> The file is now reachable from the wiki and from the head of the project
>       https://github.com/mihasighi/smtcomp14-sl
> in the directory 'bench'.

I must have missed it when looking through the repository.

> > 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.
> 
> I'll inform the SL-SMTCOMP14 group about this procedure.

It should be considered informative rather than definitive.  I believe
there is a similar procedure being conducted for strings.

Cheers,
 - Martin