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.

More Information

Location: Kent Ridge Campus

Organization: School of Computing

Department : Department of Computer Science

Employee Referral Eligible: No

Job requisition ID : 29976