Students completing this course will learn how to:
Ultimately, students should leave knowing how to use verification tools in their own research and having experienced the joy (and challenges) of writing provably bug-free code!
Your final grade will be determined by paper summaries (10%), class participation (20%), homework assignments (20%), and a final project (50%). There will not be any exams.
Most classes will have a paper reading assigned. The night before class, you will be asked to upload a brief summary of the paper’s key ideas, strengths, and weaknesses. The goal of these summaries is to give you a chance to reflect on the paper before we meet for class. When thinking about the paper, try to put yourselves in the shoes of a Program Commitee member for your favorite conference. While all of the papers we read should be quite strong, none of them are perfect. What would need to be changed to make the paper stronger? If you were putting together a program that could only accept 30% of the papers on the syllabus, would you accept this one? As a researcher, what’s the logical next step to follow-up on this work? What questions did it leave open?
Summaries will be graded on a ternary scale: Missing/Incomplete, Decent, and Impressive. If necessary, you may skip up to two paper summaries, though you are still expected to come to class prepared to discuss the corresponding papers. Each missed summary beyond the first two will affect your summary grade proportionally.
Since this is a seminar class, much of the value of the class will come from our discussions and interactions during classtime. Hence, I expect you will come to class prepared and actively engage in discussions. Participation will form an important part of your final grade.
There will be some activities that require a laptop, but the rest of the time, I would strongly discourage laptop use. It will be quite difficult to multitask on a laptop and keep up with and engage in our discussions. Plus, several studies suggest that even taking notes on a laptop can negatively impact student learning. If there is a compelling reason why you need to use your laptop during class discussions, please let me know outside of class.
Students will also be asked to sign-up to lead the discussion on several papers throughout the semester. This requires reading the paper (as usual), reading/skimming some related papers (either those preceding or following the paper), and preparing a series of discussion topics; on the plus side, you will not need to submit a summary for any paper you lead the discussion on.
Each class should consist of at most 15 minutes summarizing the key ideas in the paper, to ensure everyone is on the same page. The remainder should be discussing deeper issues: What did the authors do well? What did they miss? How does this paper relate to previous work, especially work that we’ve already discussed? What implications does it have for future work? You may also choose to spend some of the class time on highlighting interesting aspects of the specifications, code, and proofs associated with the paper. You may also propose in-class exercises related to the paper. To help you prepare, I’ll have a regular block of time set aside on Fridays at 1:00 PM, where we can spend half an hour discussing your understanding of the paper and your plans for the class session.
Because so much of our class will be based on discussion, it’s important that we maintain an open and respectful environment in class. You can vehemently disagree with someone while still respecting them and remaining civil. Everyone is coming to the class from a different background, and we will be covering some very advanced topics, so there will be topics where some people are better informed than others, but that should be an opportunity for learning, not for grandstanding or belittling others. If you do feel uncomfortable in class for any reason (including something I might do or say) please let me know.
If you miss class, then you obviously cannot participate! I know complications, conferences, and other eventualities can arise, so you can miss up to three classes without any penalty, though please try to let me know in advance. Additional absences will impact your participation grade by approximately 4% each.
There will be 3-4 homework asignments during the semester. These are
designed to give you experience using different verification tools to verify
“real” systems, since it can be hard to appreciate the strengths and weaknesses of
these tools without getting your hands dirty.
Challenge problems are optional but fun! You may also use them as a starting point of your projects.
It’s important to turn your
assignments in on time, as late assignments make it difficult to return
everyone else’s graded assignments in a timely manner. I encourage you to
start early, as verification work, like most programming tasks, often takes longer than you expect!
The deadline for any assignment can be extended by one day with a 10% penalty.
Assignments will not be accepted more than 24 hours after the due date.
Based on what you learn in this class, you will be expected to complete a substantive research project in the space of verifying complex systems.
We will be experimenting with using Piazza for discussions outside of class. Rather than emailing general questions to me, I encourage you to post your questions on Piazza, so everyone can benefit from the answer and any discussions around it.
To get in touch with me for topics or questions specific to you, you can use private posts on Piazza, or you can email me. I’ll typically be offline in the early evening, but back on in the late evenings. I typically aim to respond within 24 hours, unless it’s an emergency. Latency will be higher on the weekends.
You can also drop by my office, CIC 2121, anytime, but I may or may not be there or in a meeting. You can schedule an explicit meeting time via email, or come by during my formal office hours (Fridays from 3:00-4:00 PM).
Aside from the final research project, students are expected to complete each assignment on their own, and should be able to explain all of the work that they hand in. Copying code or proof material from other students or online sources is not allowed. However, students are encouraged to discuss assignments (in person or via Piazza) with each other at a sufficiently high level to avoid the risk of duplicating implementation or proof. Examples of this would be discussing algorithms and properties referred to in the assignment, helping other students with questions about a programming language or tool required to complete the assignment, discussing a general proof technique, or referring to an online source with useful information. If you have questions about whether something might be an issue, contact the course staff before discussing further. Please refer to the Carnegie Mellon Code for information about university policies regarding academic conduct.
Take care of yourself. Do your best to maintain a healthy lifestyle this semester by eating well, exercising, avoiding drugs and alcohol, getting enough sleep and taking some time to relax. This will help you achieve your goals and cope with stress.
All of us benefit from support during times of struggle. You are not alone. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. Asking for support sooner rather than later is often helpful.
If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.
If you have questions about this or your coursework, please let me know.