Interested applicants are invited to apply directly at the NUS Career Portal

Your application will be processed only if you apply via NUS Career Portal

We regret that only shortlisted candidates will be notified.

Job Description

The School of Computing at the National University of Singapore invites applications for a Research Fellow position in the area of formal methods, with a focus on combining interactive verification in the Lean proof assistant with SMT-based verification tools, such as Viper, Dafny, and Verus.

The successful candidate will work as a member of VERSE research lab led by A/P Ilya Sergey, doing research at the intersection of interactive theorem proving and automated program analysis, advancing the state of the art in hybrid verification systems.

The role involves:
• Leading research projects in interactive and automated verification.
• Supervising and mentoring MSc students.
• Developing and integrating verification frameworks and toolchains.
• Assisting in the preparation of competitive grant proposals.
• Collaborating with international research groups in programming languages and formal methods.

Job Requirements

• Strong expertise in at least one interactive theorem prover, preferably Lean.
• Strong background in SMT-based verification tools (experience with Viper is an advantage).
• Excellent research and publication record in formal methods or programming languages.
• Proven ability to supervise and mentor postgraduate students.
• Experience in leading collaborative research projects.
• Strong programming skills in relevant languages (e.g., Scala, Rust, OCaml, or Haskell).
• Excellent communication skills in English.

Qualifications

• PhD in Computer Science or related field, with a specialisation in formal methods, program verification, or programming languages.
• A track record of publishing in top-tier venues such as POPL, PLDI, CAV, OOPSLA, or similar.
• Demonstrated ability to carry out independent research and contribute to collaborative projects.