Overview

MemHIP is an automated verification system for memory safety and memory usage of imperative programs. It is based on a general verification system called HIP developed by our NUS collaborators.

MemHIP conducts the verification in a modular way, method by method. For each method, it verifies the method body against the given pre-/post-specifications, which capture the requirements for memory safety as well as memory usage. Our specification language is based on separation logic, but with support for user-definable (inductive) predicates specifying both structual (shape) information and numerical (size, memory size) information. Two special variables "heap" and "stk" are reserved to denote heap and stack spaces, respectively. We assume that a value of a primitive type takes 4 bytes, while the memory space required to store a value of a user-defined data type depends on the number of the fields in the type definition .

  Simple Syntax:
  program : data_declaration
            predicate_declaration
            method_declaration
  data_declaration      : data name { type name (; ...) }
  predicate_declaration : name < name(, ...) > == hip_formula
  method_declaration    : type name( type name (, ...)  )
                              requires hip_formula
                              enusres hip_formula ;
                          {
                              statment;
                              ....
                          }
  
  hip_formula  : heap_formula & pure_formula
  heap_formula : name:: < name(,...) > * heap_formula
  pure_formula : Presburger_arithmetic_formula

  statement :   numerical expression
              | v = exp                       (assignment)
              | if condition then statement else statement
              | new name(v1,v2,...)
              | method_call
              | return exp
  

Users can annotate each method with memory usage specification by variables "heap" and "stk". For example, new_list

  node new_list(int n)
      requires heap >= 8*n & n >= 0 & stk >= 12 * (n + 1)
      ensures res::ll & heap' = heap - 8 * n & stk' = stk ;
  {
      node r = null;
      if (n > 0)
      {
          r = new_list(n-1);
          r = new node(n, r);
      }
      return r;
  }
  

• Dr. Shengchao Qin, University of Teesside
• Guanhua He, Project student, Durham University
• Dr. Florin Craciun, Project research associate (one year)
• Prof. Wei-Ngan Chin, National University of Singapore
• Chenguang Luo, Ph.D student, Durham University