COMP 293 Spring 2021 Syllabus

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 053 and COMP 141 with a "C-" or better. Moreover, some level of mathematical maturity is helpful in this course.
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.

Administration

Instructor: Sepehr Amir-Mohammadian
Email:

Lecture: MW 02:00PM - 03:20PM, through video conferencing
All live class presentations and discussions during this course may be recorded. As a student in this class, please note that your participation in live class discussions may therefore also be recorded. By participating in a live class discussion you are giving your consent to this recording. Access to these recordings will be limited to faculty and the students enrolled in the class and to assist enrolled students who cannot attend the live session.
Office hours: MW 11:00AM - 01:00PM, through video conferencing
Students need to request alternate meeting times outside of scheduled office hours through email.

Video conferencing links are provided in Canvas.

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?

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

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.

Learning objectives for MSES program: The assessment plan for this course comprises the following outcomes:

"A broad understanding of problem-solving, design, and research skills necessary to operate in the interdisciplinary arena of engineering and computer science "
"Sufficient depth in an area to be able to design complex systems or pursue a more advanced degree"
"Skills necessary to engage in lifelong careers as practicing professional engineers or computer scientists"

Collection of Work for Assessment: Student work may be retained to assess how course learning objectives are being met and for accreditation purposes.

Course Material

Software Foundations, Vol.1: Logical Foundations, by Benjamin C. Pierce, et al., locally available here.
Software Foundations, Vol.3: Verified Functional Algorithms, by Andrew W. Appel, locally available here.

These are online textbooks that have 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, lectures, assignments, supplementary material, etc. will be provided through Canvas LMS.

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 for the course are assigned on the scale below:

A	A-	B+	B	B-	C+	C	C-	D+	D	F
[93,100]	[90,93)	[87,90)	[83,87)	[80,83)	[77,80)	[73,77)	[70,73)	[67,70)	[60,67)	[0,60)

Final grades will be assigned based on several performance factors. These factors and their quantitative contribution to the final grade are as follows:

Reading assignments: 0%
Homework Assignments: 25%
Class Activities: 25%
Course project and presentation: 25%
Midterm exams: 15%
Final exam: 10%

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 quizzes, discussions and labs, 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 or four exams will be conducted during the semester, 2-3 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

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. 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, without late submission penalty. Submissions after 11:59PM of the same day will be accepted within the next 24 hours with 5% penalty.
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.
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.

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

Late submission policy: Deliverables for homework assignments and the course project will be accepted up to three weekdays late, with a 5% per day penalty.
All assignments will be considered individual efforts unless otherwise specified, and will be treated as such under the Academic Honesty Policy.

Academic Honesty

The Honor Code at the University of the Pacific calls upon each student to exhibit a high degree of maturity, responsibility, and personal integrity. Students are expected to:

Act honestly in all matters
Actively encourage academic integrity
Discourage any form of cheating or dishonesty by others
Inform the instructor and appropriate university administrator if she or he has a reasonable and good faith belief and substantial evidence that a violation of the Academic Honesty Policy has occurred.

Violations will be referred to and investigated by the Office of Student Conduct and Community Standards. If a student is found responsible, it will be documented as part of her or his permanent academic record. A student may receive a range of penalties, including failure of an assignment, failure of the course, suspension, or dismissal from the University. The Academic Honesty Policy is located in Tiger Lore and online.

Course-specific Honor Code Policy: Engineering is generally a cooperative endeavor and collaborative learning can be a valuable experience for all involved. However, proper assessment (i.e., grading) requires that work be done by individuals. To balance these two requirements, the following policy will apply:

Collaborative work on course assignments is encouraged. This includes working together on planning solution strategies and helping each other to debug programs.
Collaboration must stop short of someone else writing your assignment. You may not directly copy the work of another student. You also may not copy the work of another student, and then modify it so that it does not look the same as the original author's work. It is your responsibility to ensure that the work you submit is an honest representation of your own understanding of the material.

Marginal cases will be resolved by oral examination of the student(s) involved. If they each understand the material in the assignment, it will be considered honest collaboration. If they do not, then it will be considered academic dishonesty.

In many cases, it may be possible to identify reusable source code from textbooks, web sites or other resources that can help you with assignments. You are permitted to use such references provided that:

The amount of code reused does not exceed 25% of the total assignment length, and
In the source code comments, you clearly identify any code that you did not write, state where it came from, and to what extent you modified it.

You are responsible for understanding the theory behind all algorithms or source code used, regardless of their source.

Accommodations for Students with Disabilities

If you are a student with a disability who requires accommodations, please contact the Director of the Office of Services for Students with Disabilities (SSD) for information on how to obtain an Accommodations Request Letter.

Student meets with the SSD Director and provides documentation and completes registration forms.
Student requests accommodation(s) each semester by completing the Request for Accommodations Form.
Student arranges to meet with his/her professors to discuss the accommodation(s) and to sign the Accommodation Request Letter.

To ensure timeliness of services, it is preferable that you obtain the accommodation letter(s) from the Office of SSD during the first week of class. After the instructor receives the accommodation letter, please schedule a meeting with the instructor during office hours or some other mutually convenient time to arrange the accommodation(s).

The Office of Services for Students with Disabilities is located in the McCaffrey Center, Rm. 137.

Nondiscrimination Policy

The University of the Pacific does not discriminate in the administration of any of its educational programs, admissions, scholarships, loans, athletics, or other University activities or programs on the basis of race, color, national and ethnic origin, handicap, sexual orientation or preference, sex or age.

COMP 293: Reliable Software Design

Course Description