LARA

Lecture 10 Skeleton

Guest lecture by Andrey Rybalchenko:

ASTREE Static Analyzer

A Static Analyzer for Large Safety-Critical Software

Link to paper

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

Link to paper

Combination of Abstractions in the ASTRÉE Static Analyzer