Postdoc position at Virginia Tech on OS verification

Postdoctoral Research Associate
Virginia Tech

A postdoctoral position on OS verification is available in the Systems Software Research Group at Virginia Tech's ECE Department. The project involves formally verifying components of operating systems (e.g., PREEMPT RT Linux) to meet functional and non-functional (e.g., timing) specifications using theorem proving technologies. A particular focus is to develop equivalence of component implementations (at C level) to their formal (abstract) specifications using machine-checked proofs, or automatically/semi-automatically derive machine-checked implementations from specifications.

Recent computer science or computer engineering PhD graduates with background in formal methods, verification, or theorem proving are sought. Background in Isabelle/HOL, Coq, etc., and experience with their applications (or other proof assistants/theorem provers) to production systems are particularly sought. The position is for two-year minimum, with strong possibilities for additional years, and have no teaching obligations. Contact Prof. Binoy Ravindran with a CV at binoy@vt.edu.