COS IW 05: Independent Work Seminar
|
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 techniques for formal methods (FM) and programming languages (PL) for enhancing correctness and performance. This seminar will focus on their applications in code generation, inference of specifications (such as loop invariants, method pre/post conditions, run-time assertions), and code verification via proofs.
Students in the seminar can choose from a variety of domains and an application of their own interest. For example, they can work with python/Java/C programs, or hardware designs written in Verilog, or distributed system protocols (written in a domain specific language). They can use available tools and frameworks, design a suite of benchmarks for evaluation, and experiment with different strategies to generate target programs, specifications, or proofs. Students may work on a team project, but with prior permission of the instructor, and where each student has a distinct semester-size component of the project.
There are no prerequisites for this seminar beyond COS 217 and COS 226. Students
will be expected to attend all seminar meetings. The first two seminar meetings
will provide some background on formal methods (e.g., code verification tools),
introduction to available agentic frameworks, and pointers to recent papers that
combine PL-based and ML-based techniques in automated/verifiable code generation.
The remaining meetings will be used for discussions on project proposals,
implementations, and results; with students reporting their progress each week
and doing a class presentation at the end.
| Date | Topic | Notes and Resources |
| Sep 2 | Introductions and Background | Background papers: [B1] [B2] [B3] |
| Sep 9 | Tools and Project Ideas | |
| Sep 16 | Project ideas: bring a draft for Written Project Proposal to class | |
| Sep 23 | Proposal presentations | Sep 30 | Proposal presentations, project updates |
| Oct 7 | Progress updates, discussion, and feedback | |
| Oct 14 | Discuss status of project implementation and results Discuss any issues related to the Checkpoint form |
|
| Oct 21 | Fall recess, no class | |
| Oct 28 | Discuss status of project implementation and results | |
| Nov 4 | Prepare draft of project slides | Attend "How to Give an IW Talk" earlier, on Tuesday, Nov 3 |
| Nov 11 | Final Presentations: practice talk w/demo | Attend "How to Write an IW Paper" earlier, on Tuesday, Nov 10 | -->
| Nov 18 | Final Presentations: practice talk w/demo Written Final Report: bring a draft outline to class |
|
| Nov 25 | Thanksgiving break, no class | |
| Dec 2 | Last class: discussion, suggestions Written Final Report: bring a draft of all sections to class |
We recognize the potential benefits of using (Generative) AI tools for various tasks in this seminar, ranging from initial project exploration (explaining concepts, providing summaries of prior work), to project design and implementation (code generation, testing), and final presentation and report preparation.
Indeed, we encourage projects that might use and study AI tools for various tasks in software development (e.g., code generation, debugging, testing).
This seminar allows use of AI tools, with the following requirements: