The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

Come work at with Coq at Princeton in the DeepSpec project!

[Official job posting at the end of this message]

One of our goals is to leverage the CompCert verified optimizing
C compiler in interesting ways.  For example,

* Use CompCert to compile the CertiKOS verified hypervisor kernel
 (Zhong Shao, Yale), and connect the CompCert correctness proof smoothly
  to the CertiKOS correctness proof.

* Prove correctness of C source programs in the Verifiable C program logic
  (Appel, Princeton),  not just sequential C programs but shared-memory
  concurrent, separately compiled; and connect the CompCert correctness proof
  to the Verifiable C soundness proof.

* Use CompCert's memory model in a specification and verification of the
  LLVM compiler infrastructure (Steve Zdancewic, Univ. of Pennsylvania),
  mix-and-match CompCert compiler phases with LLVM phases.

All of these projects require, of CompCert, an expressive, modular specification--not
the same specification that Xavier Leroy originally published, but a stronger one.

At Princeton we have been doing that kind of work for some time now, for example:

The CompCert Memory Model, Version 2,
by Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
INRIA Research Report RR-7987, June 2012 (also appears as a chapter in this book).

Verified Compilation for Shared-memory C, by Lennart Beringer, Gordon Stewart,
Robert Dockins, and Andrew W. Appel. 23rd European Symposium on
Programming (ESOP'14), April 2014.

Compositional CompCert, by Gordon Stewart, Lennart Beringer, Santiago Cuellar,
and Andrew W. Appel. POPL 2015: The 42nd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, pages 275-287, January 2015.

This is still much interesting research to be done on the connection of CompCert
to all these projects (CertiKOS, Verifiable C, Vellvm), and perhaps other projects.
All these projects are part of the DeepSpec consortium, and you can read about
them on the deepspec.org web site.  I encourage you to come work with us on the
engineering and application of CompCert's specification. 

Sincerely,

Andrew Appel


Postdoc or Research Engineer in Verified Software Toolchain project at Princeton The Department of Computer Science at Princeton University solicits applications for either a postdoctoral research position or a professional specialist position, in the Verified Software Toolchain project. The anticipated research is in the development and engineering of the specification and proof of the CompCert verified compiler. The ideal candidate will have experience using the Coq proof assistant or similar tools. Candidates for a postdoc position should have PhD in Computer Science or a related field. Candidates for a Professional Specialist position should normally have a Masters or PhD degree. To ensure full consideration, we encourage candidates to complete their applications, (including letters of recommendation) by February 15, 2015. (Late applications may still be considered). Applicants should submit a CV and research statement, and contact information for three references. Princeton University is an equal opportunity employer. All qualified applicants will receive consideration for employment without regard to race, color, religion, sex, national origin, disability status, protected veteran status, or any other characteristic protected by law. Finalist candidates to be hired will be required to complete a successful background check. Apply here:   https://jobs.cs.princeton.edu/postdoc-vst/