معرفی
Xinyu Feng is a Professor at the Department of Computer Science and Technology, Nanjing University, with research spanning programming languages, formal methods, and system software verification. His work focuses on developing rigorous frameworks for certifying low-level system programs, particularly those involving concurrency, preemptive threads, and hardware interrupts.
- Nanjing University, China
- Huawei (collaboration)
- Yale University, PhD in Computer Science (2007)
Research Interests: His research integrates Separation Logic and Rely-Guarantee Reasoning to create modular verification techniques for concurrent systems. Key areas include:
- Formal verification of OS kernels and hypervisors
- Concurrency control in preemptive and interrupt-driven environments
- Parameterized memory models for relaxed concurrency semantics
- Certified compilation and proof-carrying code
- Optimistic concurrency algorithms and non-blocking data structures
- Modular verification of synchronization primitives
Article Trends: His publications emphasize modular and compositional methods for concurrent program verification, with a strong focus on practical applications in system software. Recurring themes include integrating formal reasoning with real-world challenges like hardware interrupts, preemptive scheduling, and SDN programming.
Scientific Awards:
- PLDI'19 Distinguished Paper Award
Professional Leadership: Xinyu Feng has served on program committees for leading conferences (POPL, PLDI, ICFP, CAV) since 2005 and chairs sessions at events like PLDI and POPL. He actively contributes to advancing formal verification standards in the field.
