LARA

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