[Apology for possible cross-postings!] The Department of Computer Science at Yale University is seeking applicants for 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 certifying compilers. The programming languages and operating systems group, led jointly by Professors Zhong Shao and Bryan Ford 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 program logics and semantic models can best capture these abstractions? what are the right programming languages and environments for developing such certified kernel? and how to build new automation facilities to 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 PostDoc positions 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 Spring 2011). Interested applicants for PostDoc 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 yale.edu). PhD positions (with full guaranteed financial support) are also available. Applicants interested in pursuing PhD studies can email either PI but should still submit their applications directly to the Yale Graduate School of Arts and Sciences (the deadline for Fall 2011 admission is January 2nd, 2011). More information regarding this research effort can be found in a white paper available at <http://flint.cs.yale.edu/ctos> or at the two PIs' research web sites <http://flint.cs.yale.edu> and <http://dedis.cs.yale.edu>. Inquiries can be directed to any PI. Professors Zhong Shao and Bryan Ford Department of Computer Science Yale University P.O. Box 208285 New Haven, CT 06520-8285, USA Phone: +1 (203) 432 6828 and +1 (203) 432 1055 Email: zhong.shao at yale.edu and bryan.ford at yale.edu