[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
I have a number of positions available on research topics connected with
program correctness and (deductive) verification techniques and tools; these
topics touch on programming language design and semantics, formal proof
systems, logic and SMT solving in various combinations. Three representative
topics are:
1. A large ongoing effort to build verification support for the Rust
language: the Prusti project.
2. Formalising, explaining and debugging logical encodings suitable for
automated SMT solving.
3. Static analysis techniques for inferring formal specifications for
partially-specified programs.
I plan to hire a combination of MSc and PhD students, for a start in
September 2021; I may also hire up to one excellent postdoc candidate for a
similar timeframe. MSc students at UBC perform research (and sometimes
teaching) throughout their studies, and are paid a stipend in return; PhD
student positions are also fully funded.
For both MSc and PhD students, the application process is to the department
directly (naming one or more potential supervisors is encouraged), and the
deadline for this year is December 15th. Details of the programmes and
application process can be found here:
https://www.grad.ubc.ca/prospective-students/graduate-degree-programs/master
-of-science-computer-science
https://www.grad.ubc.ca/prospective-students/graduate-degree-programs/phd-co
mputer-science
In case you have any questions or would like more information about my
research, you can check out my new webpage here:
https://www.cs.ubc.ca/~alexsumm/ and are welcome to email me on
[email protected] <mailto:[email protected]>
Best wishes, Alex
