# Lecture 10 Skeleton

Guest lecture by Andrey Rybalchenko:

## 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