Nina Narodytska

*Please note: Nina will be presenting remotely. This CyLab seminar is open only to partners and Carnegie Mellon University faculty, students, and staff.

Speaker: Nina Narodytska
Staff Researcher, VMware Research by Broadcom

Talk Title:

Lemur: Integrating Large Language Models in Automated Program Verification

Joint work with Andrew Wu and Clark Barrett

Abstract: The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that typically demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.

Bio: Nina Narodytska is a staff researcher at VMware Research by Broadcom. Prior to VMware, she was a researcher at Samsung Research America. She completed postdoctoral studies in the Carnegie Mellon University School of Computer Science and the University of Toronto. She received her PhD from the University of New South Wales. She was named one of “AI’s 10 to Watch” researchers in the field of AI in 2013. She has presented invited talks and tutorials at FMCAD'18, CP'19, AAAI'20, IJCAI'20, LMML'22, CP'22 and ESSAI'23.