[Om-announce] Postdoctor​al position on Model Checking and Security at NUS

[Liu Yang]

2 Postdoc Research Fellow Positions on Model Checking and Security
National University of Singapore


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 (1 SGD = ~ 0.83 USD). Housing
allowance may also be provided.


Interested applicants should send their CV to Dr. DONG, Jin-Song  at
dongjs at comp.nus.edu.sg and Dr. LIU, Yang at liuyang at comp.nus.edu.sg.



Thanks and Regards,
Liu Yang
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://openmath.org/pipermail/om-announce/attachments/20110922/3065db60/attachment.htm