• English only

# Differences

This shows you the differences between two versions of the page.

sav07_lecture_9_skeleton [2007/04/17 19:58]
vkuncak
sav07_lecture_9_skeleton [2007/04/19 11:53] (current)
vkuncak
Line 86: Line 86:

=== Reduced product === === Reduced product ===
-
-===== ASTREE Static Analyzer =====
-
-=== A Static Analyzer for Large Safety-Critical Software ===
-
-
-Section 5.4: A remark on notation:
-  * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,​[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$.
-  * this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$.
-  * this is abstracted to abstract domain
-
-=== The Octagon Abstract Domain ===
-