Course Objectives/Student Learning Outcomes

By the end of the course, a student will be able to:

Formalize algorithms in the Coq proof assistant
Prove the correctness of algorithms.
Identify engineering tradeoffs related to assurance and developer effort.

Course Materials

There are no required textbooks, but if you find yourself wanting extra background, a variety of resources are available.

Method of Assessing Student Achievement

Grades for the course will be calculated as follows:

Six problem sets, due weekly during the first half of the semester: 30%
Project: 40%
Presentation: 15%
Reading: 10%
Class Particiation: 5%

This course uses a letter grading system, which is the official grading system at Cornell University. Typically, 80-90% of the students in this course receive a grade of A- or higher and the median grade is typically an A.

Academic Integrity

Absolute integrity is expected of all Cornell students in every academic undertaking. The course staff will prosecute violations aggressively using automatic detection tools.

You are responsible for understanding every word of these policies:

Under no circumstances may you hand in work done with or by someone else under your own name or share code with anyone else unless explicitly allowed. If you are unsure about what is permissible and what is not, please ask!

Special Needs and Wellness

It is Cornell policy to provide reasonable accommodations to students who have a documented disability (e.g., physical, learning, psychiatric, vision, hearing, or systemic) that may affect their ability to participate in course activities or to meet course requirements. Students with disabilities are encouraged to contact Student Disability Services at 607-254-4545, or the instructor for a confidential discussion of their individual needs.

If you are experiencing undue personal or academic stress at any time during the semester or need to talk to someone who can help, contact the instructor or:

Engineering Academic Advising at 607-255-7414,
Learning Strategies Center at 607-255-6310,
Let’s Talk Drop-in Counseling at Gannett at 607-255-5155
Empathy Assistance and Referral Service at 607-255-EARS.