A symbolic analysis framework for static analysis of imperative programming languages

► We present a generic symbolic analysis framework for imperative programming languages. ► Our framework computes all valid variable bindings at a given program point. ► Variable bindings are kept in an algebraic structure called supercontext. ► Path expression algebra models control flow information of programs. ► A homomorphism maps path expressions into the symbolic domain.