CS 340: Modeling for Computer Systems Syllabus
This course focuses on modeling and specifying computer systems. Students will learn how to reason about the properties and expected behavior of modern software. Topics include designing specifications, property-based testing, model finding and checking, and satisfiability solvers.
Communication
Please sign up for the course Zulip via the email you get in the first week of class. Most course announcements will happen on Zulip rather than via email. Zulip is an open-source, Slack-like chat tool with a few unique features that make it a good fit for class discussion. It's also used by many open-source systems programming communities.
Expectations
CS 340 is an upper-level, advanced elective. As such, I expect students to be comfortable with picking up new languages and tools, tackling more open-ended assignments, and completing readings that draw from a wide variety of sources. I also expect students to be comfortable installing software programs following external instructions and documentation. However, I will provide a lot of support with this initially, especially during the Workshop sessions!
CS 340 assignments can be completed on your local machine or on the Linux-based department machines. Everyone enrolled should already have a CS-Linux account from CS 240; if you have problems accessing your account, please let me know.
Text
The middle portion of the course uses the following textbook: Software Abstractions: Logic, Language, and Analysis, Revised Edition by Daniel Jackson's. A copy will be available in Workshop each week that you can access, I recommend getting your own copy if feasible.
Work
Assignments
Assignments are typically assigned on Wednesday and due the following Tuesday at midnight.
Each Wednesday, there is a 50-minute Workshop session. The workshop may have some supplemental material; but will always include some time to get started on that week's project.
Assignments come in three variants:
- Written. Text-answer assignments (interactive via Gradescope).
- Implementation. Implementation assignments can typically be completed in any programming language of your choice, as long as you have instructor permission. Permission is granted by default for two programming languages: Python and Rust. Some assignments may further restrict the implementation language.
- Modeling. In the middle portion of the course, modeling assignments are to be completed in the Alloy Analyzer. You will submit your Alloy code via Gradescope.
All assignments should be submitted via Gradescope.
Late work
This course covers a wide range of material, so I encourage you to try to submit by the listed deadline. If you need a short extension (excluding the final project deadlines), you can have one by default by filling out the 48-hour-extension request form (no further communication needed). If you need a longer extension, please reach out to me to discuss a plan. Work turned in past any discussed deadline or extension date will have a cap on the highest score you can achieve. The highest score for non-discussed late work is an 85 (that is, any score above 85 will be given an 85; lower scores will not change).
Project
In the final third of the course, students will complete an open-ended final project in groups of 2-3 (solo projects may be allowed with explicit instructor permission).
The project will have 3 milestones:
- Proposal. All project ideas must be explicitly approved by the instructor via a proposal document.
- Presentation. In the last week of class, each group will present their work so far and get peer feedback on the remaining work for their project.
- Final artifact. Each group will submit their code and a writeup describing their final artifact.
Participation
This course is small and includes frequent in-class discussion and exercises, all of which contribute to your final grade. Each lecture will have some component I'll use to help track participation. You can miss 2 lectures without it impacting your participation grade (though I would still appreciate a Zulip DM or email to let me know). After those 2, additional absences should be discussed with me for them to be considered excused.
Honor Code and Collaboration/Resource Policies
The Wellesley Honor Code applies to CS340, and combines with specific course policies to determine what level of collaboration and use of online resources is acceptable.
In general, the CS340 collaboration policy has two subparts:
1. Default for graded assignment:
- Your submitted solutions must be your own work, even if you collaborate with other students.
- For pair assignments, you must not divide work among people to complete separate parts and combine the solutions.
- Your submissions must cite all collaboration and reference material (excluding course materials and reference linked from the course website) that you used.
- You should not use generative AI (e.g., ChatGPT) without explicit instructor permission (for example, with permission a final project could analyze code generated by a ChatGPT/CodePilot).
- You may collaborate on conceptual (non-independent) aspects of the assignment with other current students, including in Workshop sessions. You may both look at code on one person's computer screen for the purposes of debugging. However, you should not copy code from another person's screen to your own submission. You must be able to fully explain any code or written work that you submit.
2. [Independent] components:
- Most assignments will have some components marked as [Independent]. On these components, you must not view another student's code, even for the purposes of debugging. You should only discuss [Independent] components with me, the instructor.
Grading
Your final grade will consist of: Course grades are computed by weighting course components as follows:
- Assignment work: 60%
- All assignments have equal weight.
- Participation & in-class exercises: 15%
- Final project: 25%
- Final project proposal 5%
- Final project presentation: 10%
- Final project code, report, and peer evaluation: 10%
The following numeric scores guarantee these letter grades (boundaries may be softened, but not made more difficult): 93.5+: A, 90.0+: A-, 86.6+: B+, 83.3+: B, 80.0+: B-, 76.6+: C+, 73.3+: C, 70.0+: C-, 60.0+: D, <60.0: no credit.
Recall that the minimum grade to earn credit under credit/no credit grading is C. The minimum grade to pass and earn credit under normal letter grading is a D.
Classroom environment
It is extremely important that this course is a respectful and supportive environment. Computer science is a wonderful and exciting field, and I hope every student in this class feels that they belong in this discipline. I expect everyone in this course to do their part to make all students feel welcome. This includes avoiding making assumptions about your classmates’ backgrounds, being professional and kind when working together, and letting me know of any issues if they arise.
Mental health
Your mental health is more important than any course. Please let me know if you would like to talk (though I am a mandated reporter). The college also has many resources available to you. If you feel you are falling behind in the course, please contact me as soon as possible to work on possible solutions.
Feedback
This is a new course this year, so I am especially open to comments and suggestions for the course! Please feel free to speak with me directly or use the anonymous feedback form if you would prefer.
Accommodations
Every student has a right to full access in this course. If you need any accommodations, please contact Wellesley’s Disability Services. If you need immediate accommodations, please arrange an appointment with me as soon as possible. If you are unsure but suspect you may have an undocumented need for accommodations, you are encouraged to contact Disability Services. They can provide assistance including screening and referral for assessments. Disability Services can be reached at disabilityservices@wellesley.edu, at 781-283-2434, by scheduling an appointment online at their website.
Religious Observance
Students whose religious observances conflict with scheduled course events should contact me in advance to discuss alternative arrangements. You may do this through the Wellesley College Religious Observance Notification system if you prefer.
Policies on Discrimination, Harassment, and Sexual Misconduct
Wellesley College considers diversity essential to educational excellence and we are committed to being a community in which each member thrives. The College does not allow discrimination or harassment based on race, color, sex, gender identity or expression, sexual orientation, ethnic or national origin or ancestry, physical or mental disability, pregnancy or any other protected status under applicable local, state or federal law.
If you or someone you know has experienced discrimination or harassment, support is available to you:
- Confidential reporting: Students can report their experiences to Health Services (781.283.2810); Stone Center Counseling Service (781.283.2839); or Religious and Spiritual Life (781.283.2685). These offices are not required to report allegations of sexual misconduct to the College.
- Non-confidential reporting:
- You can report directly to me. As a faculty member, I am obligated to report allegations of sex-based discrimination to the Nondiscrimination/Title IX Office.
- You can report directly to the Nondiscrimination/Title IX Office (781.283.2451) to receive support, and to learn more about your options for a response by the College or about reporting to a different institution.
- You can report to the Wellesley College Police Department (Emergency: 781.283.5555, Non-emergency: 781.283.2121) if you believe a crime has been committed, or if there is an immediate safety risk.
Attribution & Acknowledgments
This course draws on course material from Tim Nelson's Logic for Systems at Brown University. Assignment exercises are in some cases adapted from Daniel Jackson's Software Abstractions: Logic, Language, and Analysis. This website uses Zola and some configuration from Adrian Sampson's Advanced Programming Languages at Cornell University.