Researcher, PostDoc, and PhD Positions in the Yale FLINT Group

The Department of Computer Science at Yale University is seeking applicants for Researcher, PostDoc, and PhD positions in the broad area of certified software. The successful applicants will be expected to participate in a rigorous research program on topics such as programming languages, formal semantics, certified operating systems, program verification, proof assistants and automation, concurrency and coordination, language-based security, and certified and certifying compilers.

The programming languages and operating systems group, which is led by Professor Zhong Shao at Yale, is embarking on a multi-year effort to develop a new certified OS kernel that generalizes and unifies traditional OS abstractions in microkernels and hypervisors. The new effort advocates a modular certification framework for OS kernel components, which mirrors and enhances the modularity of the kernel itself. Using this framework, it aims to create not just a "one-off" lump of verified kernel code, but a statically and dynamically extensible kernel that can be incrementally built and extended with individual certified modules, each of which will provably preserve the kernel's overall safety and security properties.

Important research questions include but are not limited to: what OS kernel structures can offer the best support for extensibility, security, and resilience? what semantic models, program logics, and/or type systems can best capture these abstractions and kernel structures? what are the right programming languages and environments for developing such certified kernel? what new formal methods and automation facilities can make certified software really scale?

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.

Applicants for Researcher and PostDoc positions must have a Ph.D. in Computer Science or a closely related field. Interested applicants for these positions should email a CV, research statement, and the names of three references with their email addresses and phone numbers to Zhong Shao (Email: zhong.shao at

Applicants interested in pursuing PhD studies should submit their applications directly to the Yale Graduate School of Arts and Sciences (the deadline for Fall 2016 admission will be in January 2016).

More information regarding this research effort can be found at the PI's research web site (FLINT).

Professor Zhong Shao, Department of Computer Science, Yale University, P.O. Box 208285, New Haven, CT 06520-8285, U.S.A.