Please use this identifier to cite or link to this item: https://doi.org/10.1145/2048147.2048152
Title: A HIP and SLEEK verification system
Authors: Chin, W.-N. 
David, C.
Gherghina, C.
Issue Date: 2011
Source: Chin, W.-N.,David, C.,Gherghina, C. (2011). A HIP and SLEEK verification system. SPLASH'11 Compilation - Proceedings of OOPSLA'11, Onward! 2011, GPCE'11, DLS'11, and SPLASH'11 Companion : 9-10. ScholarBank@NUS Repository. https://doi.org/10.1145/2048147.2048152
Abstract: The HIP and SLEEK systems are aimed at automatic verification of functional correctness of heap manipulating programs. HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify the specifications of heap-manipulating programs. The specification language allows user defined inductive predicates used to model complex data structures. Specifications can contain both heap constraints and various pure constraints like arithmetic constraints, bag constraints. Based on given annotations for each method/loop, HIP will construct a set of separation logic proof obligations in the form of formula implications which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover for separation logic with frame inferring capability.
Source Title: SPLASH'11 Compilation - Proceedings of OOPSLA'11, Onward! 2011, GPCE'11, DLS'11, and SPLASH'11 Companion
URI: http://scholarbank.nus.edu.sg/handle/10635/41341
ISBN: 9781450309424
DOI: 10.1145/2048147.2048152
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

5
checked on Dec 13, 2017

Page view(s)

57
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.