Princeton University
Computer Science Department

Course Description

There has been an explosion of interest in using Generative AI (GenAI) tools and Large Language Models (LLMs) in software and systems development, and in combining them with logic-based formal methods for enhancing productivity and correctness. This seminar will study research advances that explore their growing applications in code generation, specification inference, verification, and testing. We will read papers from a variety of domains, including software, hardware, distributed systems, and networks. Additionally, we will also read papers that use logic-based tools, such as the Lean interactive theorem-prover, for training reasoning models.

All students are expected to lead and actively participate in class discussions – auditors are welcome! Students taking the course for credit will also do a class project (on a topic of their choice) and submit an end-of-term paper.

General Information

Location: Mon and Wed, 10:40am -- 12:00pm ET, Friend Center 009

Professor: Aarti Gupta (aartig), CS Building 209, 258-8017.

Office Hours: by appointment.

Graduate Coordinator: Louis Riehl (lriehl), CS Building 213.

Resources

Available on the Canvas course website

Course announcements, discussions, and questions are available on the Ed Discussion forum.

Grading

• Participation in class and paper reviews: 30%
• Presentation and leading discussions: 30%
• Project and end-of-term paper: 40%