Post-doc on formal verification at Boston College

Stream: job postings

[Joseph Tassarotti]

A postdoctoral position is available in the Computer Science department at Boston College under the supervision of Jean-Baptiste Tristan and Joseph Tassarotti. The candidate will join our project on the formally verified compilation of probabilistic programs.

The goal of the project is to use a proof assistant to implement a compiler for the Stan programming language and prove that the generated inference algorithm converges to the distribution specified by the input program. Our project builds upon the CompCert compiler and compiles Stan programs with a succession of well-defined program transformations. Candidates are expected to participate in the generalization of existing transformations to more features of the Stan language, the design and implementation of new transformations, the definition of the operational semantics of the intermediate languages, and the proofs of semantics preservation.

Although we envision using Coq for parts of the compiler to be able to interface with CompCert, we are open to using Lean to verify the runtime, where the proof of correctness will require developing significant results from the theory of Markov chains on continuous state spaces.

The position is available immediately, with a flexible starting date. It includes funds for travel to conferences and comes with no teaching load.

Interested candidates should apply at https://bc.csod.com/ats/careersite/jobdetails.aspx?site=1&c=bc&id=4776 and contact Jean-Baptiste Tristan <tristanj@bc.edu> and Joseph Tassarotti <tassarot@bc.edu> with a copy of their CV.