Paper Info
Title
A HIP and SLEEK verification system
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.
Year
DOI
Venue
2011
10.1145/2048147.2048152
OOPSLA Companion
Keywords
Field
DocType
automatic verification,sleek verification system,heap constraint,sleek system,specification language,separation logic proof obligation,sleek separation logic prover,automatic prover,automated verification system,separation logic,simple imperative language
Specification language,Separation logic,Programming language,Computer science,Correctness,Imperative programming,Heap (data structure),Theoretical computer science,Predicate (grammar),Gas meter prover,Verification system
Conference
Citations 
PageRank 
References 
6
0.45
6
Authors
3
Name
Order
Citations
PageRank
Wei-Ngan Chin186863.37
Cristina David224514.14
Cristian Gherghina3856.60