Resources

Software installation instructions and supplementary references will be added as they become relevant. Lecture slides and assigned readings will be linked from the schedule.

Optional textbooks

• [COC] Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
• [DP] Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2016.

Optional textbooks are available through the University of Alberta course reserves. There is no required textbook. Specific sections will be identified on the schedule when assigned.

Software

• Z3
• Dafny
• Lean
• Theorem Proving in Lean 4

Students do not need to install every tool at the beginning of the term. Installation requirements will accompany the relevant lecture or assignment.

Learning and Working Environment

The Faculty of Science is committed to ensuring that all students, faculty and staff are able to work and study in an environment that is safe and free from discrimination, harassment, and violence of any kind. It does not tolerate behaviour that undermines that environment. This includes virtual environments and platforms.

If you are experiencing harassment, discrimination, fraud, theft or any other issue and would like to get confidential advice, please contact any of these campus services:

• Office of Safe Disclosure & Human Rights: A safe, neutral and confidential space to disclose concerns about how the University of Alberta policies, procedures or ethical standards are being applied. They provide strategic advice and referral on matters such as discrimination, harassment, duty to accommodate and wrong-doings. Disclosures can be made in person or online using the Online Reporting Tool.
  
• University of Alberta Protective Services: Peace officers dedicated to ensuring the safety and security of U of A campuses and community. Staff or students can contact UAPS to make a report if they feel unsafe, threatened, or targeted on campus or by another member of the university community.
  
• Office of the Student Ombuds: A confidential and free service that strives to ensure that university processes related to students operate as fairly as possible. They offer information, advice, and support to students, faculty, and staff as they deal with academic, discipline, interpersonal, and financial issues related to student programs.
  
• Office of Student Success and Experience: They can assist students in navigating services to ensure they receive appropriate and timely resources. For students who are unsure of the support they may need, are concerned about how to access services on campus, or feel like they may need interim support while they wait to access a service, this office is there to help.