Dimitris Bouras, a first-year PhD student in the Programming Languages Lab at Peking University supervised by Prof. Sergey 

Mechtaev, has been awarded the NSFC Research Fund for Excellent International PhD Students for his project

“Verification-Aware Large Language Models: Hybrid Frameworks for Program Reasoning, Symbolic Execution, and Smart

Contract Verification”

This recognition follows the recent success of his work HoarePrompt, which has been accepted to ICSE 2026, and additional

 research milestones within the lab. HoarePrompt introduces a natural-language–guided approach to correctness reasoning.

Dimitris is also finalizing Gordian, a framework that uses LLM-generated ghost code to overcome logic bombs in symbolic execution.

Together, these achievements highlight the lab’s growing influence in combining formal verification, symbolic execution, and large 

language models toward trustworthy software systems.