Abstract

Contents

  • Theory and techniques for building a basic program verifier for a language with references to dynamically allocated objects
  • A specification style and encoding thereof