COMP 274: Reliable Software Design (Fall 2025)

aka Mechanized Software Verification

Course Description

With the technological advancements, critical systems (e.g., in the aerospace industry, healthcare industry, etc.) are being deployed and used in a widespread fashion. This trend, along with the increasing complexity of such systems, necessitate their software components to provide guaranteed reliability and assurance. This course introduces a mathematical foundation for rigorous analysis of computer programs, by exploring the logical underpinnings and the tools that are used to reason about program correctness in order to develop high quality and robust software. This is accomplished by leveraging mechanized verification tools in a hands-on manner, in particular using Coq proof assistant. Mechanized verification of programs ensures that the software is "correct", i.e., it behaves properly, using machine-checkable mathematical theorem proving. In this course, the students engage in writing programs that formally define system constructs, specify the properties of interest, and prove the satisfaction of those properties in the system.

Prerequisites: COMP 141 and COMP 147 with a "C" or better and graduate or blended students in the School of Engineering and Computer Science or instructor approval.
When enrolling in this course, you should already understand the basics of functional programming, e.g., data types, pattern matching, recursive definitions, etc. Understanding how programming language syntax and semantics work is also required. Further, you should be comfortable with basic mathematical concepts such as theorems, proofs, induction, contradiction, etc.

Website: Syllabus, Canvas LMS

Credits: 3 units

Course Catalog: hhttps://catalog.pacific.edu/search/?search=comp+274

Administration

Instructor: Sepehr Amir-Mohammadian
Email: email address
Class time/location: MW 12:30PM - 01:50PM, Chambers 214

Office hours: MW 14:00 – 15:15, Chambers 122
Students need to request alternate meeting times outside of scheduled office hours through email.

Learning Objectives

The vision for this course is: What do I, as a software engineer, need to understand about the proper behavior of programs, and how can I certify that the proper program behavior is guaranteed?

You will have many different opportunities to gain this knowledge through:

  • Hands-on classes
  • Homework assignments
  • Course projects
  • Student presentations
  • Class lectures, discussions, reading assignments, and quizzes

After taking this class, the student is expected to be able to understand:

  • the principles of functional programming, including structured data, polymorphism, higher order functions, and total/partial maps,
  • different tactics to prove the properties of programs (e.g., by induction), automation of proofs, and compositional proof techniques for program correctness,
  • logical frameworks, including constructive and classical logic,
  • how to implement different algorithms and verify them in a mechanised fashion.

Course Material

We will use the following textbook and additional resources throughout the semester:

This is an online textbook that has embedded exercises that can be worked in the Coq proof assistant. Students should use the copy hosted locally. This guarantees that the textbooks will not change for the duration of the class. The slides, assignments, supplementary material, etc. will be provided through Canvas LMS.


Major topics include:

  • An overview on logic, proof assistants, and functional programming
  • Essential elements of Coq's programming language (Gallina)
  • Proof by induction
  • Structured data definitions
  • Polymorphism and higher-order functions
  • Coq basic proof tactics
  • Logic in Coq: Constructive vs. Classical logic
  • Total and partial maps
  • Modeling programs in imperative settings
  • Extracting verified code to other programming languages
  • Proof automation
  • Examples of algorithm verification, including sorting algorithms, search trees, etc.

Grading and Attendance Policy

Grades are assigned on the scale below:

AA-B+BB- C+CC-D+DF
[93,100] [90,93) [87,90) [83,87) [80,83) [77,80) [73,77) [70,73) [67,70) [60,67) [0,60)

Final grades are based on:

  • Reading assignments: 0%
  • Attendance: 5%
  • Homework Assignments: 25%
  • Class Activities: 25%
  • Course project and presentation: 25%
  • Exam: 20%

Attendance:

  • Class attendance and participation is necessary and expected. There will be numerous activities in class, and these activities cannot be made up outside of class. Participation requires that you are properly prepared for classroom discussions, and have completed all reading assignments before the relevant class.
  • You will only be allowed three excused or unexcused class misses during the semester. The only acceptable excuses for missing a class, an assignment due date, or an exam are serious illness, family emergency or important professional, academic or athletic activities. Illness or family emergency may require documentation. Excuses for professional, academic or athletic activities must be approved by the instructor in advance. After three misses, no excuses will be accepted.
  • Students missing a class are responsible for making up the material discussed in that class on their own. Students are responsible for being aware of any announcements made during their absence.

Exams

Three exams will be conducted during the semester, 2 midterm exams and a final exam. The schedule will be announced in class and content and format will be discussed prior to the exams. Make up exams will only be scheduled in emergency situations.

Assignment Guidelines

Release and Submission

  • Reading Assignments: Reading assignments will be released on the course Canvas page one or two days before each lecture session. Students are encouraged to study the referred material before each class session. There are not any submissions for reading assignments.
  • Class Activities: Class activities are group-based and they will be released on the course Canvas page. Each group cannot exceet 2 students in size. The goal is to accomplish all lab activities and submit in Canvas until the end of each session. However, submissions are accepted until 11:59PM on the same day. Submissions after 11:59PM of the same day will NOT be accepted.
  • Homework Assignments: Homework assignments will be released on the course Canvas page with a clearly indicated due date. Timely submissions are accepted until 11:59PM on the due date. Homework assignments are group-based with max size of 2 students per group.
  • Course Project and Presentation: Course project and presentation will be released on the course Canvas page with a clearly indicated due date. Timely submissions are accepted until 11:59PM on the due date. Course projects are also group-based with maximum two students per group.

Solutions: Solutions to homework assignments, class activities, and exams may be submitted electronically via Canvas, or in class on pencil-and-paper when appropriate.

Late policy: Deliverables for homework assignments and course projects will be accepted up to three days late, with a 5% per day penalty.
All work is individual unless otherwise specified, and subject to the Academic Honesty Policy.

Academic Honesty

The Honor Code calls upon each student to exhibit maturity, responsibility, and integrity. Students are expected to:

  • Act honestly in all matters
  • Encourage academic integrity
  • Discourage cheating or dishonesty
  • Inform the instructor/administration with good‑faith evidence of violations

Violations are referred to the Office of Student Conduct and Community Standards and may result in penalties up to failure/suspension/dismissal. See Tiger Lore and online policy.

Course‑specific policy:

  • Collaboration on planning/strategy/debugging is encouraged.
  • Do not submit someone else’s work.

Marginal cases may be resolved via oral examination to assess individual understanding.

Accommodations for Students with Disabilities

If you require accommodations, visit pacific.edu/disabilities to contact SSD and request services.

  1. New students: apply via New Students Apply Here.
  2. Returning students: request letters each semester via Returning Students Login Here.

SSD: McCaffrey Center (2nd Floor) • 209‑946‑3221 • ssd@pacific.edu • website

Nondiscrimination Policy

The University of the Pacific does not discriminate in the administration of its programs/activities based on race, color, national and ethnic origin, handicap, sexual orientation or preference, sex, or age.

The instructor reserves the right to change these policies and guidelines at any time, and students agree to abide by the most recent version of this syllabus.

Back to top