Synthesising Functional Invariants in Separation Logic

Ewen Maclean, Andrew Ireland, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We describe the CORE system which automatically proves fully functional specifications about pointer programs, generating functional parts of the invariants automatically where necessary.
Original languageEnglish
Title of host publicationWING 2010. Workshop on Invariant Generation 2010
EditorsAndrei Voronkov, Laura Kovacs, Nikolaj Bjorner
Number of pages2
Publication statusPublished - 2012

Publication series

NameEPiC Series in Computing


Dive into the research topics of 'Synthesising Functional Invariants in Separation Logic'. Together they form a unique fingerprint.

Cite this