[TYPES/announce] Postdoc Positions at The University of Pennsylvania

[Steve Zdancewic]

PENN’S PL CLUB IS LOOKING FOR POSTDOCS

The University of Pennsylvania’s PL group is looking to hire several
postdoctoral researchers to work on projects related to verification,
software specification, and security.

START DATES: Negotiable, beginning as early as January 2018.

DURATION: All positions are one year, with the possibility of extension
to a second year.

QUALIFICATIONS: Applicants should have a Ph.D. in computer science and a
strong background in topics related to - formal verification and
specification - programming languages, type systems, and semantics - the
Coq theorem prover - the specific project topics described below.


APPLICATION PROCEDURE:

-   Upload a CV, statement of interest, and the names of three letter
     writers to: https://goo.gl/forms/SMu8KmtdHjXKnqWF3

-   Direct your letter writers to submit their letters via:
     https://goo.gl/forms/ElgimgzvDh4C2scu1

-   Contact Steve Zdancewic (mailto:stevez at cis.upenn.edu) if you have any
     questions.

DEADLINE: Applications will be considered starting on _1 December 2017_
and will be considered until all the positions are filled.

Successful applicants will join the University of Pennsylvania’s PL Club
with opportunities to collaborate on the DeepSpec project and other
ongoing activities.



POTENTIAL RESEARCH PROJECTS


DeepWeb - A Formally Verified Web Server

Penn is coordinating a large-scale verification effort that combines
technologies from across the DeepSpec project with the aim creating a
verified web server: the high-level specification is in terms of the
HTTP protocol, and the implementation will be high-performance C
software (verfied using Princeton’s VST) hosted by Yale’s CertiKOS,
which will itself be run on top of MIT’s verified implementation of the
Risc V hardware. This project will tie together specification,
verification, and testing across multiple levels of abstraction.


Vellvm II - Verified LLVM

The Vellvm project is building a (verified LLVM), a framework for
reasoning about programs expressed in LLVM’s intermediate representation
and transformations that operate on it. Vellvm provides a mechanized
formal semantics of LLVM’s intermediate representation, its type system,
and properties of its SSA form. Specific research topics include:
developing modular semantics for low-level control-flow-graph and SSA
representations; extending the model to account for concurrency;
building a “decompiler” from SSA to a higher-order functional language;
or using the LLVM semantics to verify correctness of compiler analyses,
optimization passes, and security-relevant program transformations.


QuickChick - Property-Based Testing for Coq

The QuickChick project investigates the interplay between formal
specification / verification and property-based random testing a la
Haskell QuickCheck. The QuickChick tool (a QuickCheck-like testing
framework for Coq) is heavily used in the DeepSpec project, for example
as the specification framework for an executable formal specification of
HTTP and related protocols. We are experimenting with using this
specification as a bug-finding tool, both for industrial web servers and
for initial prototypes of our own server. This requires addressing both
foundational and engineering challenges, in the testing technology and
in the creation of specifications that are suitable for both
verification and testing.


Programming Languages for Differential Privacy

Penn boasts a longstanding and energetic collaborative research effort
on putting new privacy technologies – particular statistical techniques
such as differential privacy – into practice, involving faculty,
students, and postdocs from programming languages, distributed systems,
and algorithms, and machine learning. Topics of interest include
privacy-protecting type systems and static analyses, distributed
implementations of private algorithms, program logics for privacy, and
formal verification of randomized algorithms.



THE UNIVERSITY OF PENNSYLVANIA


Penn’s department of Computer and Information Science offers a vibrant
research environment with a long tradition of excellence in programming
languages and related areas. We are located in Philadelphia, a city that
offers a rich array of cultural, historical, and nightlife attractions,
parks and outdoor recreation, convenient public transportation, and
affordable housing.