Highly motivated applicants are being sought to work on developing model checking techniques. The postdocs will work with the software engineering and formal methods group at National University of Singapore on further developing the PAT toolkit (http://www.patroot.com).

PAT is a powerful self-contained framework for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstraction techniques, and model checking techniques can be easily supported. Currently, 11 modules supporting different domains have been developed, covering concurrent, real-time, probabilistic, hierarchical systems. It offers a library of model checking algorithms for a variety of properties, e.g., reachability analysis, temporal logic verification, refinement checking, verification with fairness, zone abstraction, probabilistic model checking, etc. PAT has been applied to many case studies and successfully found previously unknown bugs. It has been adopted for research and teaching in multiple universities. More details about PAT can be found at http://www.patroot.com.


The applicant shall conduct research related to model checking techniques and security verification. Following list is the possible topics.
1 Verify security systems: security protocols, web security, TPM, security device, etc.
2 Software and assembly code verification.
3 Code synthesis for security procotols.
3 PAT optimization using techniques like distributed/parallel model checking, automated abstraction techniques (possibly domain specific), generalized symmetry reduction, etc.
The applicant will study the PAT framework, identify the suitable state reduction techniques, design/implement the techniques in PAT.


The position involves conducting basic research, developing tools, working as part of a research team, traveling, and giving presentations. The working language is English.


Candidate profile:
- A PhD in Computer Science or related areas is required.
- Expertise in Formal Methods, Model Checking technology and Security.
- Strong background in logic and discrete math.
- Strong programming skills (the language we are working with is C#).
- An established research record.


The post-doc positions are funded by large research projects in School of Computing and Temasek Laboratories, National University of Singapore.
The term is currently 3 years starting immediately and can be extended.
The salary range is around 60K-92K SGD pa. Housing allowance may also be provided.


Interested applicants should send their CV to [email protected]