Ways to obtain invariants
•Programmer-supplied
•Static analysis: examine the program text [Cousot][Gannod]
–properties are guaranteed to be true
–pointers are intractable in practice
•Dynamic analysis: run the program
–complementary to static techniques
[Joke] I have heard that some programs lack exhaustively-specified invariants; we’ll assume for the rest of the talk that we have such invariants.

Claim:  programmers have these in mind, consciously or unconsciously, when they write code.  We want access to that hidden part of the design space.

We might want to check/refine/strengthen programmer-supplied invariants, and the program may be modified/maintained.  (Leveson has noted that program self-checks are often ineffective.)

May want to check/strengthen programmer-supplied assertions.
Static analysis:
•For instance, abstract interpretation.
•The results of a conservative, sound analysis are guaranteed to be true.
•Static techniques can’t report true but undecidable properties.  (or properties of a program context)
•Pointers:  problematic to represent program state and the heap; must approximate, resulting in too-weak results.
Dynamic techniques are complementary to static ones.