Indian Institute of Technology Bombay

Ph.D. Project Openings 2021

  • Available project openings

    As of now there is 1 project opening available.

    1. Project Title: An Abstraction-Refinement based Translation Validator for GCC Compiler (GCC Validator)
      No. of Positions: 1
      Project Description:

        The reliability of an executable code critically depends on the reliability of the compiler used to generate the executable. Translation validation provides guarantees on the reliability of specific runs of a compiler by showing that it transforms a source program into a semantically equivalent target program. We want to build an end-to-end Translation Validation tool that takes as input a C program, and automatically proves or disproves the following for a run of the GCC compiler with all optimizations enabled: (a) The behavior of the program before and after each machine-independent intraprocedural optimization pass (called tree optimizations in GCC) are equivalent. (b) The behavior of the tree-optimized GIMPLE program (the intermediate representation of GCC) is equivalent to the register transfer language (RTL) program obtained by the expansion pass of GCC. (c) The behavior of the program before and after each machine dependent RTL-optimization pass are equivalent. (d) If the semantics are not equivalent for any of the above passes, the tool will generate a counterexample as a witness. We will evaluate the effectiveness of our translation validator on the standard benchmark, SPEC2006.

      For more information about this project, please refer to this presentation. (Here are the accompanying slides.)