Relational Semantics of Procedures

Procedure Contracts and Their Meaning

Reasoning about Procedures by Inlining Contracts, even in presence of recursion (can ignore the shunting rules part)

Octagons as an example of a relational abstract domain. Concept of polyhedra.

Use of relational domains for interprocedural analysis sketched, but not explained in detail.

Reachable pushdown configurations are regular (only sketched)