Compilers and Their Role in Software Analysis and Verification

Recall the big picture in Verification as Science. What is the role of the compiler?

Compiler is the closest relative of a program analysis and verification system: they both manipulate programs taking into account the meaning of statement constructs.

  • they have same initial phases

Compiler front-end = program analyzer front-end:

  • tokenization (lexical analysis)
  • parsing (syntax analysis)
  • creating abstract syntax trees
  • resolving identifiers
  • translation to intermediate form

Differences in goals:

  • compiler generates executable object code
  • analyzer answers questions about the source code

Natural way of integrating them:

  • perform front-end operations
  • ask analyzer: is program meaningful?
  • try to optimize the code, ask analyzer: do conditions that enable optimization hold?
  • perform code generation

More on Compilers