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:

  1. Written. Text-answer assignments (interactive via Gradescope).
  2. 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.
  3. 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:

  1. Proposal. All project ideas must be explicitly approved by the instructor via a proposal document.
  2. 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.
  3. 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:

2. [Independent] components:

Grading

Your final grade will consist of: Course grades are computed by weighting course components as follows:

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:

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.