Research Fellow/Engineer (in the area of verification of quantum programs) (ICT/LSW)

As a University of Applied Learning, SIT works closely with industry in our research pursuits. Our research staff will have the opportunity to be equipped with applied research skill sets that are relevant to industry demands while working on research projects in SIT.

The primary responsibility of this role is to deliver on a research project, funded by Singapore Ministry of Education (MOE), where you will be part of the research team to develop a scalable and comprehensive framework for formal verification of quantum programs. The framework consists of the following deliverables:
• Intermediate Language. We plan to develop an intermediate language to model quantum programs. The intermediate language would be complete to describe all the desired characteristics of quantum computing while at the same time simple enough to be understood by most programmers.
• Formal Verification Framework. We plan to develop a comprehensive framework to verify the correctness of quantum programs written in the proposed intermediate language.
• Mechanization. We plan to mechanize the formal framework using state-of-the-art theorem provers such as Coq or Isabelle/HOL.
• Proof Automation. We plan to develop formal methods for automatic reasoning that can be materialized into commercial tools.

Key Responsibilities:

• Participate in and manage the research project with Principal Investigator (PI) and the research team members to ensure all project deliverables are met.

• Undertake these responsibilities in the project:
1. develop an intermediate language to write quantum programs.
2. develop a comprehensive framework to verify the correctness of quantum programs written in our intermediate language.
3. mechanize the verification framework using state-of-the-art theorem provers such as Coq or Isabelle/HOL.
4. develop formal methods for automatic reasoning that can be materialized into commercial tools.

• Carry out Risk Assessment, and ensure compliance with Work, Safety and Health Regulations.
• Coordinate procurement and liaison with vendors/suppliers.
• Work independently, as well as within a team, to ensure proper operation and maintenance of equipment.

Job Requirements:

• Have relevant competence in the areas of formal methods (including theorem proving and model checking, especially theorem proving), quantum computing, and software analysis/verification.
• Have a degree in computer science, computer engineering, or related areas. Possessing a Master’s or PhD degree will be advantageous
• Knowledge of separation logic and quantum program analysis/verification will be advantageous.

Key Competencies:

• Able to build and maintain strong working relationships with people within and external to the university.
• Self-directed learner who believes in continuous learning and development
• Proficient in technical writing and presentation
• Possess strong analytical and critical thinking skills
• Show strong initiative and take ownership of work

Major Challenges:

As quantum computers are operated in extreme physical conditions and thus the cost per run is significantly high, it is desirable to verify the correctness of a quantum programs before the execution. However, the verification task of quantum programs is challenging due to the following reasons:

• Quantum programs (even written at high-level languages) are complicated to comprehend as it requires a good understanding of quantum mechanics and the relevant advanced mathematics.
• The quantum states are exponentially huge in size because the state of a classical bit is either 0 or 1 at any time, while the state of a quantum bit (qubit) can be in the superposition, where both states 0 and 1 can co-exist simultaneously. This induces the state explosion problem for brute-force-like methods.
• Quantum states are naturally probabilistic thus may yield different results on different runs, which is challenging for the testing and debugging methods.