AI-Assisted Discovery of Implicit Program Knowledge for Deductive Verification

Forschungsthema:	Deductive Verification
Typ:	MA
Datum:	2026-10-30
Betreuer:	Tianhai Liu
Aushang:

Deductive program verification often requires auxiliary knowledge that is not explicitly represented in source code or program specifications. Such knowledge may include mathematical relationships, data-structure properties, semantic abstractions, and auxiliary lemmas.

This project investigates whether large language models can identify such knowledge from Java programs and their verification tasks, and whether it can improve automated proof search in KeY.

Students will identify relevant categories of implicit knowledge, investigate methods for representing the generated knowledge as proof obligations or verification annotations, and evaluate their effectiveness on selected Java verification problems.

Particular attention will be given to knowledge that differs from conventional loop invariants.

References

Huan Zhao, Haoxin Tu, Zhengyao Liu, Martin C. Rinard, and Abhik Roychoudhury. 2026. Automated Lemma Discovery in Agentic Program Verification. In Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE '26). Association for Computing Machinery, New York, NY, USA, 323–335. https://doi.org/10.1145/3832783.3834356