Specification and Verification of Programs with Pointers (Part 1)

  • Rustan Leino

Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR |

Published by Microsoft Research

Download BibTex

Basic verifier architecture

  • Source language
  • Intermediate verification language
  • Verification condition (logical formula)