LARA

This is an old revision of the document!


Modular analysis of procedures

Inlining specifications. Last part of SAV07 Homework 4.

Postconditions that refer to values of variables in the precondition.

The meaning of modifies clauses.

ASTREE Static Analyzer

The Octagon Abstract Domain

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

Combination of Abstractions in the ASTRÉE Static Analyzer