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.
Website: Syllabus, Canvas LMS
Credits: 3 units
Course Catalog: http://catalog.pacific.edu/search/?search=comp+293
Semester: Fall 2018
Instructor:
Sepehr Amir-Mohammadian
Email: [at] (samirmohammadian) ([dot] (pacific) (edu))
Lecture: TR 1:00PM-2:20PM, CTC 113
Office hours: TR 2:30PM-4:30PM, CTC 118
Students need to request alternate meeting times outside of scheduled office hours through email.
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:
After taking this class, the student is expected to be able to understand:
Learning objectives for MSES program: The assessment plan for this course comprises the following outcomes:
Collection of Work for Assessment: Student work may be retained to assess how course learning objectives are being met and for accreditation purposes.
We will use the following textbooks for this course:
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, assignments, supplementary material, etc. will be provided through Canvas LMS.
The following topics will be discussed in this course:
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:
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 activities, and have completed all reading assignments before the relevant class. 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. 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.
Two exams will be conducted during the semester, a midterm- 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.
Release and Submission
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 course projects 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.
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:
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:
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:
You are responsible for understanding the theory behind all algorithms or source code used, regardless of their source.
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.
3-Step Accommodation Process:
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.
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.