[Om-announce] Postdoc Research Fellow Positions Available on Model Checking, Security and Program Analysis in Singapore

[Liu Yang (Asst Prof)]

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 in Singapore on further developing the PAT toolkit (http://www.patroot.com<http://www.patroot.com/>).

The applicant shall conduct research related to model checking techniques and security. Following list is the possible topics.
# Verify security systems: security protocols, web security, TPM, security device, etc.
# Program analysis in both source level and binary level, particularly for Malware analsyis
# Android security
# Formal modelling and verification of multi-agent systems and trust management
# Distributed/parallel model checking algorithms
# Model checking abstraction and reduction techniques.
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, Program Analysis 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 Nanyang Technological University.
The term is currently 1 year starting immediately and can be extended to 3 years.

Interested applicants should send their CV to Dr. LIU, Yang at yangliu at ntu.edu.sg<mailto:yangliu at ntu.edu.sg>.

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, 20 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<http://www.patroot.com/>.



________________________________
CONFIDENTIALITY:This email is intended solely for the person(s) named and may be confidential and/or privileged.If you are not the intended recipient,please delete it,notify us and do not copy,use,or disclose its content.

Towards A Sustainable Earth:Print Only When Necessary.Thank you.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://openmath.org/pipermail/om-announce/attachments/20130506/cad89657/attachment-0001.html>