Lecture 10 Skeleton
ASTREE Static Analyzer
A Static Analyzer for Large Safety-Critical Software
Section 5.4: A remark on notation:
- if denotes the state and is a deterministic statement, then represents the new state after executing the statement; the relation corresponding to statement semantics would be .
- this function is extended to map sets of states to sets of states, which gives function mapping to and is what we called strongest postcondition .
- this is abstracted to abstract domain