LARA

Lecture 11: Procedures: Semantics, Specifications, and Analysis

Relational Semantics of Procedures

Procedure Contracts and Their Meaning

Reasoning about Procedures by Inlining Contracts

Frame Conditions and Invariants

Specification Variables and Data Abstraction

Notion and Uses of Specification Variables

Specification Variables for Public Interfaces

Controlling When Invariants Hold

Soundness of Simple Ghost Variables

References on Interprocedural Analysis

Two Approaches to Interprocedural Analysis

Generating precise and concise procedure summaries

Compositional May-Must Program Analysis: Unleashing the Power of Alternation