CyLab Seminar
— 1:00pm
Location:
In Person and Virtual - ET
-
Hamburg Hall A301 and Zoom
Speaker:
NINA NARODYTSKA
,
Staff Researcher, VMware Research by Broadcom
https://research.vmware.com/researchers/nina-narodytska
Lemur: Integrating Large Language Models in Automated Program Verification
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.
Joint work with Andrew Wu and Clark Barrett
—
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. Faculty Host: Corina Pasareanu
In Person and Zoom Participation.
⇒ This seminar is open only to partners and Carnegie Mellon University faculty, students, and staff.
Event Website:
https://www.cylab.cmu.edu/events/2024/02/05-seminar-narodytska.html