[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