Syllabus🔗

Programming Language Technologies and Paradigms, CMSC 433

Term: Fall, 2025

Professor: Anwar Mamat (he/him)

Email: anwar@umd.edu

Office Hours: By appointment. Send email or ELMS message to set up.

Prerequisite: a grade of C or better in CMSC330; and permission of department; or CMSC graduate student.

Credits: 3.

Lectures: TuTh 11:00am-12:15pm CSI 1115 (AM), TuTh 3:30pm - 4:45pm IRB 0318 (AM)

Course Description: CMSC 433

Students will be introduced to a range of modern formal methods and software engineering practices, focusing on Dafny, SAT solvers, Solver aided programming, and computer aided theorem proving. The first part of the course will look at Dafny, a verification-aware programming language that is used heavily at Amazon: students will learn different techniques for writing down precise specifications of desired system behavior and for proving that specifications hold of software artifacts. The second part of the course will focus on SAT solvers, SMT solvers, and apply these techniques to automatic bug finding and program verification. We will implement a miniature version of Dafny. The third part of the course will focus on the interactive theorem proving. We will learn the basics of the theorem prover Coq. Knowledge of functional programming in the form of OCaml (from 330) is assumed, but not prior knowledge of Dafny.

Contents:

1 Course Workflow🔗

The course will be based on live lectures and discussion. The main forms of communication will be ELMS (for main course announcements and grades) and Piazza.

2 Office Hours🔗

Office hours format will be announced closer to the start of the semster.

3 Topics🔗

4 Grading🔗

Grades will be maintained on ELMS.

You are responsible for all material discussed in lecture and posted on the class web page, including announcements, deadlines, policies, etc.

Your final course grade will be determined according to the following percentages: Your final course grade will be determined according to the following percentages:

Final letter grades will be assigned based on the following cutoff table:

5 Assignments🔗

There will be several programming assignments, often with full week given for completion and submission (e.g. if it assigned on a Tuesday it will be due the following Tuesday at 11:59pm EST unless otherwise noted).

Assignments will be submitted through Gradescope.

6 Quizzes & surveys🔗

There will be many quizzes and surveys. These will be administered through ELMS. Completed surveys receive full credit. Instructors reserve the right to reject survey responses that are not considered thoughtful.

7 Exams🔗

There will be a midterm exam on Oct 23 and a final exam on Dec 15

8 Gradescope🔗

Programming projects can be developed on your own system and subitted via Gradescope, which will provide virtual machines suitably configured for running your code. All project submissions must work correctly on the Gradescope VMs, and your projects will be graded solely based on their results on those machines. Because language and library versions may vary with the installation, in unfortunate circumstances a program might work perfectly on your system but not work at all on the VMs. Thus we strongly recommend that as you develop any project, you should run it several days early on Gradescope to have time to address any compatibility problems.

9 Outside-of-class communication with course staff🔗

Course staff will interact with students outside of class in primarily two ways: office hours, and electronically via e-mail. The use of Piazza and/or other classroom forums is allowed, and discussion amongst the students is encouraged, as long as the discuss is about the concepts and not the solutions. The majority of communication should be via office hours.

Personalized assistance, e.g., with assignments or exam preparation, will be provided during office hours. Office hours for the instructional staff will be posted on the course web page.

Additional assistance will provided via discussion on Piazza. You may use this forum to ask general questions of interest to the class as a whole, e.g., administrative issues or problem set clarification questions. The course staff will monitor it on a daily basis, but do not expect immediate answers to questions. Please do not post publicly any information that would violate the university academic integrity policy (e.g., problem set code).

Personal e-mail to TAs should be reserved for issues that cannot be handled by the above methods.

Important announcements will be made in class or on the class web page, and via Piazza.

10 Excused Absences🔗

For medical absences, you must furnish documentation from the health care professional who treated you. This documentation must verify dates of treatment and indicate the timeframe that the student was unable to meet academic responsibilities. In addition, it must contain the name and phone number of the medical service provider to be used if verification is needed. No diagnostic information will ever be requested. Note that simply being seen by a health care professional does not constitute an excused absence; it must be clear that you were unable to perform your academic duties.

It is the University’s policy to provide accommodations for students with religious observances conflicting with exams, but it is the your responsibility to inform the instructor in advance of intended religious observances. If you have a conflict with one of the planned exams, you must inform the instructor prior to the end of the first two weeks of the class.

For missed exams due to excused absences, the instructor will arrange a makeup exam. If you might miss an exam for any other reason other than those above, you must contact the instructor in advance to discuss the circumstances. We are not obligated to offer a substitute assignment or to provide a makeup exam unless the failure to perform was due to an excused absence.

The policies for excused absences do not apply to project assignments. Projects will be assigned with sufficient time to be completed by students who have a reasonable understanding of the necessary material and begin promptly. In cases of extremely serious documented illness of lengthy duration or other protracted, severe emergency situations, the instructor may consider extensions on project assignments, depending upon the specific circumstances.

Besides the policies in this syllabus, the University’s policies apply during the semester. Various policies that may be relevant appear in the [Undergraduate Catalog](http://www.umd.edu/catalog).

If you experience difficulty during the semester keeping up with the academic demands of your courses, you may consider contacting the Learning Assistance Service in 2201 Shoemaker Building at (301) 314-7693. Their educational counselors can help with time management issues, reading, note-taking, and exam preparation skills.

11 Students with Disabilities🔗

Students with disabilities who have been certified by Disability Support Services as needing any type of special accommodations should see the instructor as soon as possible during the schedule adjustment period (the first two weeks of class). Please provide DSS’s letter of accommodation to the instructor at that time.

All arrangements for exam accommodations as a result of disability must be made and arranged with the instructor at least three business days prior to the exam date; later requests (including retroactive ones) will be refused.

14 University of Maryland Policies for Undergraduate Students

Please read the university’s guide on [Course Related Policies](https://www.ugst.umd.edu/courserelatedpolicies.html%22), which provides you with resources and information relevant to your participation in a UMD course.

12 Academic Integrity🔗

The Campus Senate has adopted a policy asking students to include the following statement on each examination or assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this examination (or assignment)." Consequently, you will be requested to include this pledge on each exam and assignment. Please also carefully read the Office of Information Technology’s policy regarding acceptable use of computer accounts.

Assignments and projects are to be completed individually, therefore cooperation with others or use of unauthorized materials on assignment or projects is a violation of the University’s Code of Academic Integrity. Both the person receiving assistance and the person providing assistance are in violation of the honor code. Any evidence of this, or of unacceptable use of computer accounts, use of unauthorized materials or cooperation on exams or quizzes, or other possible violations of the Honor Code, will be submitted to the Student Honor Council, which could result in an XF for the course, suspension, or expulsion.

• For learning the course concepts, students are welcome to study together or to receive help from anyone else. You may discuss with others the assignment or project requirements, the features of the programming languages used, what was discussed in class and in the class web forum, and general syntax errors. Examples of questions that would be allowed are "Does a cond expression always end with an else-clause?" or "What does a ’mismatched parenthesis’ error indicate?", because they convey no information about the contents of an assignment.

• When it comes to actually writing an assignment, other than help from the instructional staff, assignments must solely and entirely be your own work. Working with another student or individual, or using anyone else’s work in any way except as noted in this paragraph, is a violation of the code of academic integrity and will be reported to the Honor Council. You may not discuss design of any part of an assignment with anyone except the instructor and teaching assistants. Examples of questions you may not ask others might be "How did you implement this part of the assignment?" or "Please look at my code and help me find my stupid syntax error!". You may not use any disallowed source of information in creating either the design or code. When writing assignment you are free to use ideas or short fragments of code from published textbooks or publicly available information, but the specific source must be cited in a comment in the relevant section of the program.

Violations of the Code of Academic Integrity may include, but are not limited to:

• Failing to do all or any of the work on a project by yourself, other than assistance from the instructional staff.

• Using any ideas or any part of another person’s project, or copying any other individual’s work in any way.

• Giving any parts or ideas from your project, including test data, to another student.

• Allowing any other students access to your program on any computer system.

• Posting solutions to your projects to publicly-accessible sites, e.g., on github.

• Transferring any part of an assignment or project to or from another student or individual by any means, electronic or otherwise.

If you have any question about a particular situation or source then consult with the instructors in advance. Should you have difficulty with a programming assignment you should see the instructional staff in office hours, and not solicit help from anyone else in violation of these rules.

It is the responsibility, under the honor policy, of anyone who suspects an incident of academic dishonesty has occurred to report it to their instructor, or directly to the Honor Council.

Every semester the department has discovered a number of students attempting to cheat on assignments, in violation of academic integrity requirements. Students’ academic careers have been significantly affected by a decision to cheat. Think about whether you want to join them before contemplating cheating, or before helping a friend to cheat.

You may not share, discuss, or compare assignment solutions even after they have been graded since later assignments may build upon earlier solutions.

13 Course Evaluations🔗

If you have a suggestion for improving this class, don’t hesitate to tell the instructor or TAs during the semester. At the end of the semester, please don’t forget to provide your feedback using the campus-wide [CourseEvalUM](https://www.courseevalum.umd.edu/) system. Your comments will help make this class better.

14 Right to Change Information🔗

Although every effort has been made to be complete and accurate, unforeseen circumstances arising during the semester could require the adjustment of any material given here. Consequently, given due notice to students, the instructors reserve the right to change any information on this syllabus or in other course materials. Such changes will be announced and prominently displayed at the top of the syllabus.

15 Course Materials🔗

Portions of the course materials are based on material developed by Dr. Adam Chlipala and Dr. Rustan Leino.