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

Martin Brain martin.brain at cs.ox.ac.uk
Tue May 27 08:22:18 EDT 2014

On Tue, 2014-05-27 at 11:07 +0200, Viktor Kuncak wrote:
> Dear Mihaela and Martin
> Thank you for the comments. The discussion on separation logic is very
> interesting because it brings another view to problems for which
> otherwise one would normally use array theories, possibly with
> quantifiers. Postponing for the moment the issues of the SL-SMT
> marriage arrangements, let me just note two somewhat orthogonal
> points.
> Regarding this point:
> "3. A paper giving the semantics of the theory has been written and is
> currently under submission to FMCAD."
> If the content of this report is to be used as an argument for
> community discussion, it should probably be made available as a
> technical report. This would not interfere in any way with the FMCAD
> reviewing process (in case this is still relevant).

Cesare has posted a link to the technical report version:


At the moment I can't see a link from the main SMT-LIB site to it.  

 - Martin

More information about the SMT-COMP mailing list