[TYPES/announce] Postdoc position at Colorado in data-driven program analysis with potential industrial applications

[Bor-Yuh Evan Chang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Programming Languages and Verification Group at the University of
Colorado Boulder (CUPLV) is looking for exceptional candidates for a
postdoctoral research associate working in the area of data-driven program
analysis. This position presents a unique opportunity for potential
industrial application in collaboration with GitHub.

The ideal candidate has a background in the area of programming languages
and verification, as well as being interested in extending his or her
research to machine learning.

The postdoctoral research associate will collaborate with professors
Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Sergio Mover, as well as
engineers at GitHub. The researcher will have an opportunity to lead a
project on program repair and will contribute to potential technology
transfer with our industrial partner.

To apply, please send an email to Bor-Yuh Evan Chang <
evan.ch...@colorado.edu> or Sriram Sankaranarayanan 
with a CV and contact information for two or three references.

Our group has active projects in areas such as the following:
  - program analysis
  - program synthesis
  - cyberphysical systems

Compensation is highly competitive and commensurate with experience.
Teaching opportunities will be available.

For more information about our group, please see .

Boulder, located at the base of the Rocky Mountains, is consistently
awarded top-rankings for health, education, and quality of life.  It is
also home to a concentration of high-tech industry and to a vibrant
start-up community. It is located 30 miles from downtown Denver.

[TYPES/announce] Postdoc Positions at KTH and Chalmers on Cyber-Physical Systems (with CakeML)

[Magnus Myreen]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are looking to employ postdocs, one at KTH and one at Chalmers, to
conduct research in a joint expedition project titled:

   High-Confidence Formal Verification of Real Cyber-Physical Systems:
   from Models to Machine Code

The overall goal of this project is to develop new theoretical
foundations for formally verified cyber-physical domain-specific model
compilation, from high-level real system models down to machine code,
satisfying both functional and temporal constraints.

The project is a collaboration between:
 - Associate Professor David Broman at KTH, Sweden
   https://people.kth.se/~dbro/
 - Associate Professor Magnus Myreen at Chalmers, Sweden
   http://www.cse.chalmers.se/~myreen/

At KTH, this project will use the Coq proof assistant to design and
develop a verified model-checker and a synthesis mechanism that
correctly extracts an executable timed intermediate form (ETIF) from
high-level models of cyber-physical systems.

At Chalmers, this project will involve using the HOL4 interactive
theorem prover to develop a compiler partly from scratch and partly
from parts of the existing CakeML compiler. The new compiler's input
language is to be compatible with the ETIF from above.

To apply and read more, see the separate job ads:
 - KTH: https://goo.gl/f9HheP
 - Chalmers: https://goo.gl/SB8V3X

Application deadline: 28 February, 2019

Starting date: preferably in the first half of 2019

Both postdoc positions are for two years. The funding comes from the
Wallenberg Artificial Intelligence, Autonomous Systems and Software
Program (WASP). For more information, see
http://wasp-sweden.org/17-post-doc-positions-expedition/.

Please contact David (d...@kth.se) and Magnus (myr...@chalmers.se)
for more information.

[TYPES/announce] Postdoctoral Researcher in Programming Languages and Machine Learning at Penn State

[Danfeng Zhang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a 1-2 year full-time Postdoctoral Research 
position in differential privacy in the Computer Science & Engineering 
Department at Penn State. The position involves statistical and/or formal 
verification of differentially private algorithms, including the development of 
tools and theories for analyzing source code using programming languages and 
statistical methods.

As differential privacy gains increased acceptance in industry and government 
agencies as a methodology for protecting privacy, there is an increased need 
for tools for verifying correct code and detecting bugs in incorrect code. In 
this project, we explore program verification techniques (e.g., type systems) 
to prove differential privacy for sophisticated algorithms, as well as methods 
for generating counterexamples when the proof fails. See below for our recent 
papers in this direction:
CCS’18: http://www.cse.psu.edu/~dbz5017/pub/ccs18.pdf
POPL’17: http://www.cse.psu.edu/~dbz5017/pub/popl17.pdf

Please apply at https://psu.jobs/job/83998 
An applicant should possess a doctoral degree in Computer Science or Statistics 
and have strong background in one or more of the following areas: machine 
learning, programming languages, non-parametric statistics, differential 
privacy. The candidate must have an excellent track record of original research 
and the ability to work as part of a team. The postdoc will be provided with 
competitive salary and employment benefits. The initial appointment will be for 
one year, with an option to renew for a second year. 

Inquiries about the position should be directed to Daniel Kifer and Danfeng 
Zhang at c...@psu.edu . Applicants should upload a resume 
with at least two names of references. Applications will be reviewed until the 
position is filled.

[TYPES/announce] CS@max planck: The new Max Planck Graduate Center for Computer and Information Science

[Maria Christakis]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CS@max planck is a new Max Planck wide graduate program that allows
admitted students to work with CS faculty at any Max Planck Institute
and offers them the full range of CS research and faculty in one
program.

Specifically, CS@max planck is a highly selective doctoral program
that grants admitted students full financial support to pursue doctoral
research in the field of computer and information science, with faculty
at Max Planck Institutes and some of the best German universities.

To qualify for the program, students must hold a Bachelor's or
Master's degree in computer science (or a related field) and have an
outstanding academic record. We especially encourage applications
from students who wish to explore research across the CS spectrum
before committing to a topic and advisor.

For more information about CS@max planck, see here:

https://www.cis.mpg.de/graduate-programs/cs-max-planck

For information about other doctoral programs offered by Max Planck
Institutes, see here:

https://www.cis.mpg.de/graduate-programs/

The next upcoming application deadline is December 31, 2018.