Recruitment

Positions described below are open as of 26 Oct 2024 and will remain open until filled.

I am hiring for multiple open PhD student and postdoc positions in formal methods, with a focus on deductive verification and interactive theorem proving across various topics.

Topics of interest include:

Trustworthy automated reasoning
Goal: To build practical, formally verified certification mechanisms and frameworks for automated reasoning tools (see here).
Examples: AAAI'24, IJCAR'24
Verification of (randomized) algorithms
Goal: To formally verify state-of-the-art automated reasoning algorithms, where either the algorithm or the system being analyzed (or both) have probabilistic behavior.
Examples: CAV'24 (distinguished paper award)
Verification of hybrid systems and control
Goal: To develop and apply logics for control-theoretic reasoning in hybrid systems, and to mechanize these developments in a proof assistant.
Examples: HSCC'22 (best paper and RE award), PhD thesis (distinguished dissertation award)
Compiler verification and optimization
Goal: To enhance the verified CakeML compiler and associated tools, especially in support of the above goals.
Examples: JFP, PLDI'23
I am also interested in formalized mathematics, computer-aided cryptography, and formalization in theoretical computer science.

Please also take a look at my home page (publications, tools, etc.) for a more detailed sampling of my interests.

General requirements

I am looking to work with students / postdocs with background and research interests in formal methods.

Candidates with adjacent background, e.g., relevant topics in logic, mathematics, or computer science, are also welcome.

All positions are fully funded with competitive stipends/salaries.

They are based in Singapore and require fluency in English. (PhD students have specific requirements, see below)

Most of the topics will also require working with proof assistants such as Isabelle/HOL, HOL4, and KeYmaera X. Prior experience in interactive proofs is helpful but not mandatory.

Note: Please feel free to email me for a preliminary chat even if you are unsure of your plans. (PhDs are a long-term commitment!)

For example, I may be able to offer a (limited) number of shorter-term positions for strong candidates.

PhD students

Multiple fully-funded PhD student positions are available at the College of Computing and Data Science (CCDS), Nanyang Technological University, Singapore.

Candidates must apply and be admitted to the NTU CCDS PhD programme, including meeting all of the admission requirements.

There are two intakes each year (August and January) with respective application deadlines.

Please email me directly at tanyongkiam+recruitment@gmail.com for a discussion before you apply.

Include a CV, a brief description of your academic background (especially any prior research experience), and the research topic(s) you intend to work on for your PhD.

Other supporting material can be included as needed.

(Bonus) Pick a recent paper involving formal methods (perhaps even one of mine), write a 1 to 2 page critique of it, and attach it in your email.

Postdocs

Multiple research scientist positions are available at the Institute for Infocomm Research, A*STAR, Singapore.

The scientists are expected to work closely with our group based at A*STAR and NTU on the topics above.

All applicants must have a PhD or be close to graduating with one.

The PhD degree must be in a relevant field, e.g., Computer Science or Mathematics, and the thesis research must be relevant / adjacent to formal methods.

Positions are tenable for two years each (with possibility of extension).

Please email me directly at tanyongkiam+recruitment@gmail.com for an initial informal discussion.

It would be helpful if you shared your CV, a brief description of your current research (with pointers to relevant papers), and what you intend to work on as a postdoc with me.