[TYPES/announce] Post-Doctoral and Researcher Positions at Yale University

[Zhong Shao]

The Department of Computer Science at Yale University is seeking
applicants for multiple Post-Doctoral and Researcher positions in the
area of programming languages and formal methods. Successful
applicants are expected to participate in a rigorous research program
on topics such as certified operating systems, program verification
and synthesis, quantitative resource analysis, language-based
security, quantitative security analysis, proof assistants and
automation, concurrency and coordination, and certified compilers.

Projects in this research program are led by Zhong Shao, Eric
Koskinen, and Jan Hoffmann. In addition, the new PostDocs and
Researchers will collaborate with other Yale faculty members as well
as 12 PhD students and PostDocs who are currently members of the
research group. Most projects center around several multi-year research
efforts:

- CertiKOS: Application of cutting-edge programming language theory to
  support compositional layered development of certified system
  software (e.g., OS kernels, hypervisors, real-time embedded systems,
  distributed systems).

- DeepSpec: Development of modern specification languages (and
  compilers) for rigorous system design and certified program
  synthesis.

- CURB and SOUCIS: Detection of space/time related security
  vulnerabilities in Java Bytecode using (semi-)automatic static
  resource analyses.

- Push/Pull: Theoretical foundations for concurrent programming with
  transactions.

Successful applicants should have a combination of creativity,
self-motivation, and strong interests on applying programming language
theory or formal methods to solve practical problems. While we
encourage all interested candidates to apply, knowledge in one or more
of the following areas would be beneficial:

- Formal reasoning about concurrency and distributed computation
- Proof assistants and functional programming
- Certified compiler and program analysis
- Design and development of low-level system software
- Static resource analysis
- Quantitative security analysis
- Implicit computational complexity
- Mathematical/logical foundations of automatic verification 
- Deduction, composition, and abstraction for verification
- Model-based development of real-time embedded systems
- Security protocol and information flow control

Applicants must have a Ph.D. in Computer Science or a closely related
field. The term of a PostDoc position is one year with an option to
renew for up to four years. Starting date is negotiable (a preference
will be given to those who can start by Summer 2015).

Interested applicants should email a CV, research statement, and the
names of three references with their email addresses and phone numbers
to <pl-application at cs.yale.edu> .

More information regarding the research program can be found at the
PIs' research web sites at

  http://www.cs.yale.edu/~shao
  http://ibm.biz/koskinen
  http://www.cs.yale.edu/~hoffmann

Inquiries can be directed to any PI.

------------------------------------------------------------------------
Zhong Shao, Professor 
Department of Computer Science      Office: (203) 432-6828
Yale University                     FAX:    (203) 432-0593
51 Prospect Street                  Email:  shao-zhong at cs.yale.edu
New Haven, CT 06520-8285, USA       WWW:    http://www.cs.yale.edu/~shao
------------------------------------------------------------------------