Syllabus

Program Analysis: Theory and Practice - CSCI 7135 - Fall 2025

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Class meetings are held on Tuesdays and Thursdays from 9:30 a.m. to 10:45 a.m. in DLC 1B20.

Following University guidelines, CSCI 7135 Fall 2025 is an in-person course. All course meetings, including lectures, recitations, and office hours are in-person by default. Please communicate with the course staff in person or through Piazza for all course related matters. Please do not email any members of the course staff. You can post privately on Piazza for confidential discussions to an individual or “Instructors” to reach the course staff.

Course Overview and Goals

Are you interested in how automated reasoning is applied to modern software systems?

Program analyses have long been the foundation of compilers and programmer-productivity tools. In recent years, they have taken increasing importance in software engineering, where they are used to detect bugs in automated code reviews, flag security vulnerabilities, enforce coding standards, and even automatically generate code. Program analysis techniques are used in formal verification to prove properties of programs and increasingly as agents in generative AI systems. The course will cover the principles and practice of program analysis, focusing on both theoretical foundations and practical applications.

This seminar course is designed to acquaint you with the fundamental ideas behind program analysis. The goal is to introduce you to both the theoretical underpinnings and practical implementations of static program analysis.

Ultimately, you should come away with the ability to apply program analysis techniques to your own projects.

The course has two broad topics:

  • Program Analysis Foundations
  • Research Applications

The first part of this course focuses on foundational concepts in static program analysis, such as set constraints, dataflow, and abstract interpretation. We will take an approach that interleaves practical implementation experience with theoretical development.

The second part of the course covers special topics broadly drawn from current research in program analysis, including both static and dynamic techniques. Students will have opportunity to suggest topics of interest.

Students will also complete a final project to explore the implementation of advanced abstract domains and gain experience in applying analysis techniques.

We will be experimenting with the Lean programming language as the implementation language for this course. Lean is a functional programming language with a strong type system and support for formal verification.

Prerequisites

The prerequisites for this course are programming and mathematical experience.

The ideal programming experience is functional-programming experience from an undergraduate programming languages (e.g., CSCI 3155) and/or an undergraduate compilers course (e.g., CSCI 4555). The ideal mathematical experience is familiarity with logic and programming language semantics (e.g., CSCI 5535).

These prerequisites are not strict, and the intent is to develop this course into one accessible to a wider audience. However, your desire to be exposed to this material is very important.

Beginning graduate students and advanced undergraduates may consider taking this course.

Requirements

The course consists of the following learning activities:

  • Class Participation (10%). Participation includes both in-class and online discussion. See below for expectations for class participation.
  • Assignments (40%). There will be assignments.
  • A Final Project (50%). In the second half of the course, your time will be spent on a final project. You will create a final project that explores, extends, or experiments with the ideas in the course.
  • Reading. There will be required papers or book chapters to read.

Regrades

Any concern about an error in grading must be submitted within one week of when it is returned. Any coursework submitted for reconsideration may be regraded in its entirety, which could result in a lower score if warranted. To request a regrade, please go to the Instructor’s office hours with your coursework and an explanation of what you believe the grading error to be.

Make-Up Policy

There will be no special or make-up examinations or assignments for any student (except in the case of emergency or the stated religious observances).

Redo Policy

This course is an active learning course, which means the learning is driven primarily by active discovery in doing the assignments. To encourage iteration until mastery, you may “redo” any assignment via an oral interview with the Instructor for a maximum of 90%. In a “redo interview,” the instructor is probing for your level of understanding and may ask different questions than you have seen previously. A “redo” must be completed within one week of when the assignment is returned. You may request one interview per assignment. However, you may discuss your solutions with the instructors in office hours as much as you like before requesting your regrade. You must submit your assignment on time to participate in a “redo”.

Extra Credit and Participation

Extra credit opportunities may be offered during the course semester. Extra credit is recorded separately from normal grades and are only considered after final grades have been calculated. If your final grade is just below a grade cutoff, extra credit may bump you up to the next grade. Finding a bug in the course materials that is then adopted is a standing offer for extra credit.

Evaluation

Both your ideas and also the clarity with which they are expressed matter—both in your English prose and your code!

We will consider the following criteria in our grading:

  • How well does your submission answer the questions? For example, a common mistake is to give an example when a question asks for an explanation. An example may be useful in your explanation, but it should not take the place of the explanation.
  • How clear is your submission? If we cannot understand what you are trying to say, then we cannot give you points for it. Try reading your answer aloud to yourself or a friend; this technique is often a great way to identify holes in your reasoning. For code, not every program that “works” deserves full credit. We must be able to read and understand your intent. Make sure you state any preconditions or invariants for your functions (either in comments, as assertions, or as require clauses as appropriate).

Expectations for Class Participation

Classes focus on discussion, so it is certainly important to participate in class and read the readings beforehand.

Students are expected to be active participants in class and in the online forums (e.g., around at least 1 substantive post per week). You may and are encouraged to post comments or questions about the reading before the class where we will cover it. Posting early will help focus our discussion.

Here are some examples of good comments:

  • Questions about the reading or the class discussion.
  • Thoughtful answers to other people’s questions.
  • Clarification of some point discussed in class.
  • Thoughtful comments on a web resource related to a reading or class discussion that caught your attention (e.g., you happened upon an interesting blog post related to our discussion). Note that simply giving a link is not considered a thoughtful comment.

If everything from a class meeting seems clear to you, try to come up with a question that tests your classmates’ understanding. Put yourself in the position of an Instructor!

Overall, the intent is for you to to take a moment to reflect upon the day’s reading or class discussion. The course staff will read all posts but may not respond to all of them (e.g., if we believe your classmates’ answers are sufficient).

Textbook and Resources

Textbook

Some of our readings will come from the following text:

The following are other resources on program analysis:

We will also make use of class notes and research papers as appropriate.

Programming Language Semantics

For background resources on programming language semantics, here are a few texts:

Lean

Tools

Website

The primary channel for course materials is the course website that will link to other resources.

Canvas

We use Canvas primarily for managing grades. You should have been automatically enrolled.

Gradescope

We use Gradescope for assignment submissions. You enroll in Gradescope through Canvas.

GitHub

We use GitHub for distribution of some programming assignments. You create your GitHub assignment repositories through Canvas.

Piazza

We use Piazza for online, outside-of-class discussion. Rather than emailing questions to the course staff, questions should be posted on Piazza. I encourage you to make class-wide posts whenever possible, but there is an option to send an instructor-private message. You enroll with Piazza through Canvas.

Computing

You may use the Department’s cloud-computing environment coding.csel.io. We strongly suggest you use a Unix-based development environment as a back up (e.g., Ubuntu Linux, macOS). While not officially supported, we will try to help with other installs. Please feel free to ask for help on the forum and help by contributing your experience.

Integrity of the Course Materials

The development effort in the course materials, including the lab assignments, the exercises, and the exams, is significant. You agree that you will not share any course materials publicly or privately outside of your teams. The course materials, include your or anyone else’s solutions to the lab assignments, exercises, and exams. In particular, you agree not to post your solutions to the lab assignments in a public source code repository, such as public GitHub repositories. Use the private source code repositories provided to you for your work.

Note that there is no conflict with the Collaboration Policy described below. You are welcome and encouraged to support each other in the learning of the material.

Collaboration Policy

You are welcome and encouraged to work together in learning the material. If you worked with someone on an assignment, or if your submission includes quotes from a book, a paper, or a web site, you should thank the source. Bottom line, feel free to use resources that are available to you as long as the use is reasonable and you cite them in your submission. However, copying answers directly or indirectly from solution manuals, web pages, your peers, or even a course staff member is certainly unreasonable. If you have any doubts in this regard, please ask the course staff.

You are allowed to discuss homework assignments with other students. However, in order to ensure that the work you submit is still your own, we insist that you adhere to a whiteboard policy regarding these discussions: you are not allowed to take any notes, files, or other records away from the discussion. For example, you may work on the homework at the whiteboard with another student, but then you must erase the whiteboard, go home, and write up your solution individually. We take your ability to recreate the solution independently as proof that you understand the work that you submit.

This policy is our attempt to balance the tension between the benefits of group work and the benefits of individual work. We ask that you obey the spirit of the policy, as well as the letter: ensure that all work you submit is your own and that you fully understand the solution. This is in your best interest: the exam constitutes a significant part of your final grade and it will draw heavily on the terminology, concepts, and techniques that are exercised in the homework. It is unlikely that you will be able to do well on the exam if you do not take full advantage of the learning opportunity afforded by the homework assignments.

Academic Dishonesty Policy

We will go by the Honor Code set forth by the University. Academic sanctions may include, but is not limited to, a zero for the assignment or a failing grade for the course.

Generative AI

Follow the above Collaboration Policy when using generative AI tools such as ChatGPT, GitHub Copilot, or similar. Apply the whiteboard policy. You may use these tools as collaborators to help you understand concepts, but you must not submit their output as your own work. If you use such tools, you must clearly provide appropriate citations.

Summary

  1. Cite your sources.
  2. Inspiration is free. You may discuss homework assignments with anyone. You are especially encouraged to discuss solutions with your instructor and your classmates.
  3. Plagiarism is forbidden. The assignments and code that you turn in should be written entirely on your own. Copying/soliciting a solution to a problem from the internet or another classmate constitutes a violation of the course’s collaboration policy and the Honor Code and will result in an F in the course and a trip to the Honor Council.
  4. Do not search for a solution online or via AI. You may not actively search for a solution to the problem from the internet. This includes posting to sources like StackExchange, Reddit, Chegg, etc. Searching for basic techniques in programming is totally fine. If you want to post and ask, “How do I group by two columns, then do something, then group by a third column?”, that’s fine. What you cannot do is post, “Here’s the problem my prof gave me. I need to convert Age in Earth years to Martian years and then predict the person’s favorite color. Give me code!” That’s cheating.
  5. When in doubt, ask. We have tried to lay down some rules and the spirit of the collaboration policy above. However, we cannot be comprehensive. If you have doubts about this policy or would like to discuss specific cases, please ask an instructor. If it has not been described above, you should discuss it with us first.

Classroom Norms

We trust and expect everyone to behave in a civil and courteous manner.

In class, the course staff promises their undivided attention and reciprocally expects the same from you. In today’s world, this promise requires turning off transmitting devices, such as mobile phones and wi-fi on notebook computers. The use of notebook computers should be discussed with the instructor and they should be used only for purposes directly relevant to the class discussion. Please notify the course staff if you encounter behavior that distracts from your learning.

Classroom Behavior

We will also go by the policies set forth by the University:

Both students and faculty are responsible for maintaining an appropriate learning environment in all instructional settings, whether in person, remote or online. Those who fail to adhere to such behavioral standards may be subject to discipline. Professional courtesy and sensitivity are especially important with respect to individuals and topics dealing with race, color, national origin, sex, pregnancy, age, disability, creed, religion, sexual orientation, gender identity, gender expression, veteran status, political affiliation or political philosophy.

For more information, see the classroom behavior policy, the Student Code of Conduct, and the Office of Institutional Equity and Compliance.

Accommodation for Disabilities, Temporary Medical Conditions, and Medical Isolation

We will also go by the policies set forth by the University:

If you qualify for accommodations because of a disability, please submit to your professor a letter from Disability Services in a timely manner so that your needs can be addressed. Disability Services determines accommodations based on documented disabilities. Information on requesting accommodations is located on the Disability Services website. Contact Disability Services at 303-492-8671 or dsinfo@colorado.edu for further assistance. If you have a temporary medical condition, see Temporary Medical Conditions on the Disability Services website.

If you have a temporary illness, injury or required medical isolation for which you require adjustment, please contact the course staff to discuss your situation.

Preferred Student Names and Pronouns

We will also go by the policies set forth by the University:

CU Boulder recognizes that students’ legal information doesn’t always align with how they identify. Students may update their preferred names and pronouns via the student portal; those preferred names and pronouns are listed on instructors’ class rosters. In the absence of such updates, the name that appears on the class roster is the student’s legal name.

Honor Code

We will also go by the policies set forth by the University:

All students enrolled in a University of Colorado Boulder course are responsible for knowing and adhering to the Honor Code. Violations of the Honor Code may include but are not limited to: plagiarism (including use of paper writing services or technology [such as essay bots]), cheating, fabrication, lying, bribery, threat, unauthorized access to academic materials, clicker fraud, submitting the same or similar work in more than one course without permission from all course instructors involved, and aiding academic dishonesty. Understanding the course’s syllabus is a vital part in adhering to the Honor Code.

All incidents of academic misconduct will be reported to Student Conduct & Conflict Resolution: StudentConduct@colorado.edu. Students found responsible for violating the Honor Code will be assigned resolution outcomes from the Student Conduct & Conflict Resolution as well as be subject to academic sanctions from the faculty member. Visit Honor Code for more information on the academic integrity policy.

Religious Observances

We will go by the policies set forth by the University:

Campus policy requires faculty to provide reasonable accommodations for students who, because of religious obligations, have conflicts with scheduled exams, assignments or required attendance. Please communicate the need for a religious accommodation in a timely manner.

See the campus policy regarding religious observances for full details.

We will try to accommodate religious conflicts in a reasonable manner. Please check the exam dates and submit all requests for adjustments within the first four weeks of class. To discuss a special accommodation, please contact the Course Manager with your request.

Mental Health and Wellness

The University of Colorado Boulder is committed to the well-being of all students. If you are struggling with personal stressors, mental health or substance use concerns that are impacting academic or daily life, please contact Counseling and Psychiatric Services (CAPS) located in C4C or call (303) 492-2277, 24/7.

Free and unlimited telehealth is also available through Academic Live Care. The Academic Live Care site also provides information about additional wellness services on campus that are available to students.

CU Community of Care

CU Boulder is committed to a community of care in which students are supported by faculty and staff throughout their college journey. You don’t have to face academic challenges alone – CU and the college are here to help you learn and succeed in your coursework and campus life. Part of this community of care is your connection to faculty and staff across campus. Our college promotes and hopes you will connect with faculty or staff who may reach out during your educational journey at CU.

Course Alerts

This course participates in the CU Course Alert process to help connect you with support resources and identify your barriers to success

If you receive a course alert for this class, please see the course staff in office hours or schedule a meeting.