At Huawei Dresden Research Center (DRC), our mission is to explore programming models, operating system and virtualization technologies on multicore heterogeneous architectures and NVM/SCM platforms, aiming to provide a high-performance, reliable abstraction layer for efficient resource utilization. Collaborating with top universities and industry partners, we turn research into real-world impact—published at elite conferences (ASPLOS, OSDI) and deployed across Huawei’s global products. Join our diverse, fast-growing team of 40 experts from 10 countries and shape the future of technology in Dresden. Join us as a Formal Verification PhD Student (m/f/d) Your mission Explore cutting-edge research in formal methods theory and industry practice. Learn to propose and investigate promising new research directions and questions. Master both academic and industry reporting and writing styles for maximum impact. Learn to independently solve challenging research problems with significant industry or academic impact. Present your work at top-tier academic conferences and to internal stakeholders. Apply formal methods to industrial projects and contribute to practitioner-ready verification tools. Your areas of expertise A completed Master Degree in Computer Science or other related disciplines Familiar with one of these languages: C, C++, Rust Good understanding of multicore programming and its challenges such as performance, scalability, and correctness Good understanding of mainstream OS technologies and system software Excellent communication skills and the ability to work in multicultural and distributed teams Fluent in written and spoken English Preferred Qualifications: Experience with compilers, assembly (x86/Arm/RISC-V) Experience with systems, concurrency, weak-memory models Knowledge of formal verification tools for model checking and theorem proving such as Spin, UPPAAL, Coq, Isabelle, Z3 Publications in the fields of formal verification and theory of programming languages Experience in hosting or participation in scientific research projects or practical projects related to formal verification By applying to this position, you agree with our RECRUITMENT PRIVACY STATEMENT. You can read in full our recruitment privacy statement via the link below. http://career.huawei.com/reccampportal/portal/hrd/weu_rec_all.html Your rewards of working here Our culture is characterized by innovative power and team spirit as well as the intensive exchange of knowledge and experience within our global network. We offer healthy meals ranging from traditional Chinese to western delicacies in our famous company canteen. To keep your development ongoing, you will find a broad range of training opportunities. Many online and face-to-face training programs incl. language courses in German and Mandarin. Our diverse and welcoming environment is shaped by different backgrounds and around 40 individual nationalities. Self-responsible work in a competent, motivated and constantly growing team. Please send your application and CV (incl. cover letter and reference letters) in English. Huawe i is a leading global information and communications technology (ICT) solutions provider. Driven by a commitment to operations, ongoing innovation, and open collaboration, we have established a competitive ICT portfolio of end-to-end solutions in Telecom and enterprise networks, Devices and Cloud technology and services. Our ICT solutions, products and services are used in more than 170 countries and regions, serving over one-third of the world's population. With 197,000 employees, Huawei is committed to develop the future information society and build a Better Connected World. DRC Publications during the past years: [1] VSync by Oberhauser et al., ASPLOS’21, distinguished paper award: https://dl.acm.org/doi/10.1145/3445814.3446748 [2] CLoF by Chehab et al., SOSP’21: https://dl.acm.org/doi/10.1145/3477132.3483557 [3] CAAT by Ponce de Leon et al., OOPSLA’22, best paper award: https://dl.acm.org/doi/abs/10.1145/3563292 [4] BBQ by Wang et al. ATC’22 https://www.usenix.org/conference/atc22/presentation/wang-jiawei [5] Atomig by Beck et al. ASPLOS’23 https://dl.acm.org/doi/10.1145/3575693.3579849 [6] BWoS by Wang et al., OSDI’23 https://www.usenix.org/conference/osdi23/presentation/wang-jiawei