[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:

http://smtlib.cs.uiowa.edu/papers/BTRW13.pdf

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

Cheers,
 - Martin




More information about the SMT-LIB mailing list