PhD student focusing on Scalable Quantum Program Verification

Descrizione

Testo originale dell'annuncio (in inglese)

Are you interested in working in formal verification and programming language techniques applied to quantum systems, with the support of competent and friendly colleagues in an international environment? Are you looking for an employer that invests in a sustainable working environment and offers safe, favourable working conditions? We welcome you to apply for a PhD position at the Department of Information Technology, Uppsala University. The Department of Information Technology holds a leading position in both research and education at all levels. We are currently Uppsala University's third largest department, with 350 employees, including 120 teachers and 120 PhD students. Approximately 5,000 undergraduate students take one or more courses at the department each year. You can find more information about us on the Department of Information Technology website . The position is hosted in a research environment which includes verification experts (Parosh Abdulla, Mohammed Faouzi Atig, Bengt Jonsson, Philipp Ruemmer, Kostis Sagonas, Wang Yi), as well as experts in programming languages (Johannes Borgström, Eva Darulova, Lars-Henrik Erikson, Sofia Ouhbi, Tjark Weber, Tobias Wrigstad). The department is known for both strong theoretical work as well as tool development in these areas (UPPAAL, Concuerror, Nidhugg and other tools), publishing in top conferences such as POPL, PLDI, ICALP and CAV. Project description As both private and public investment in quantum computing continues to surge, the steady upscaling of quantum hardware (now reaching thousands of qubits) has resulted in increasingly sophisticated quantum software pipelines. Given the strategic use of quantum software (e.g. in security), there is an urgent need for verifying the trustworthiness of quantum programs at scale. Features of modern quantum programs such as Quantum Error Correction lead to hybrid quantum-classical architectures, resulting in new challenges for verification. Current tools and techniques do not offer the desired combination of scalability, automation and guarantees to verify such programs. The project aims to address this gap by combining techniques from classical verification and programming language theory with those for complex arithmetic, in order to contribute both theoretical insights and software artifacts advancing the state of the art in quantum program verification. Duties The doctoral student will primarily devote their time to doctoral education. Other departmental duties of at most 20%, including teaching and administration, may also be included in the employment. Requirements To meet the general entry requirements for doctoral studies, you must: hold a Master’s (second-cycle) degree in computer science or mathematics or a related field, or have completed at least 240 credits in higher education, with at least 60 credits at Master’s level including an independent project worth at least 15 credits, or have acquired substantially equivalent knowledge in some other way. The University may permit an exemption from the general entry requirements for an individual applicant, if there are special grounds (Chapter 7, § 39 of the Higher Education Ordinance). For special entry requirements, please see the subject’s general study plan . We are looking for candidates with: a mathematical background, excellent problem-solving skills, high motivation and capacity to persistently work on difficult problems, interest in programming, good communication skills with sufficient proficiency in oral and written English, ability to work both independently and collaboratively. Additional qualifications Experience or coursework in one or more of the following areas is considered an advantage: formal methods, programming language theory or semantics, logic, automata theory, automated theorem proving, and quantum computing. Rules governing PhD students are set out in the Higher Education Ordinance chapter 5, §§ 1-7 and in Uppsala University's rules and guideline