PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

22, Sep, 2010: Two Posrdoc Positions on Model Checking at National University of Singapore

Two Postdoc Research Fellow Positions on Model Checking
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://pat.comp.nus.edu.sg).

PAT is a powerful self-contained system for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstract techniques, and model checking techniques can be easily supported. Six modules supporting different domains have been develoed, covering concurrent, real-time, probabilistic, hierachical 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://pat.comp.nus.edu.sg.

The applicant shall conduct research on optimizing PAT. Candidate techniques include 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 lanugage is English.

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

The term is currently 2 years starting immediately and can be extended.
The salary range is around 60K-85K SGD pa (1 SGD = ~ 0.75 USD).

Interested applicants should send their CV to Dr. Jin-Song Dong at dongjs@comp.nus.edu.sg.