Link Search Menu Expand Document
Azadeh Farzan

Software Verification

(Fall 2023, under construction)

General Information

  • The course forum (access code will be provided on Quercus)
  • Grades (of non-Markus items) are posted on Quercus.
  • For textbooks and references see here.
  • Markus (becomes active on September 15)

Instructor Contact

Azadeh Farzan: azadeh at cs dot toronto dot edu

(Read the communication guidelines before sending emails)

TA Team

Nick Feng
Logan Murphy
Avery Laird

Note: Do not email your TAs. It is not in their contract to answer emails. They are contracted to communicate with you on the course forum and during office hours and tutorials.

Class Time/Location

  • Tuesdays 3-5pm in MP 137
  • Wednesdays 3-5pm in MP 134
  • Joint Tutorials: Fridays 3-5pm in MP 200 (typically the tutorial slot, but there will be exceptions)

Office Hours

Fridays 4:10-5, in class, if nothing else is anounced.

Grading Scheme

See here.

The Goal of the Course and Learning Objectives

In this course, we aim to expose you to a variety of techniques used to ensure software reliability. These techniques range proving programs correct using theorem provers (involves a lot of contribution from the user) to testing (fully automatic). We do this by:

  • covering theoretical foundations of various verification and testing techniques, and
  • putting your theoretical knowledge to practical use by using a variety of tools to solve small scale (classroom-sized) problems. This gives you a chance to practice the theory, and to get to know these tools that may be useful to you in your future careers.

This process will involve learning to use tools in a relatively short period of time (12 weeks). It may seem a bit overwhelming for some. Given the fact that most of you are about to graduate and start your new careers, this situation simulates what you will face very soon in your work environment. Computer science is a very dynamic field. New programming languages, environments, tools and techniques find their way to the market every day. As a computer scientist, you need to have to skill to catch up with the new technology quickly (in contrast to knowing one or two of these very well from your school days). The majority of students catch up and do extremely well. The small minority (about or under 20% of students) may give up trying because they think they cannot handle it. You can!

Also, in case you are taking this course as an elective, and do not like the general idea of it, then please reconsider. There are other elective courses. This course involves theory and proofs. It can be challenging for those who have a not-so-perfect background in logic and discreet math from the courses in year 1 and 2.

Communication Guidelines

Read before sending an email. Any email that does not meet the following specification will be ignored and left unanswered.

  • Email your instructor for personal matters, or asking for special considerations. These are generally considered to be rare occasions.
  • All technical (non-personal) questions should be posted on the course forum (on Piazza), so that everyone can benefit from the question and the answer.
  • Always sign your full name (as it appears on university records) at the bottom of your emails.
  • Always send your email from your university account.
  • Always include CSC410 in the subject line so that the email goes to the right folder.
  • Include your Markus handle in any Markus-related enquiries.
  • Your questions will generally be answered within two working days (excluding weekends), although this may take longer during busy times (such as around assignment due dates). So, do not rely on getting a same-day answer.

Providing Feedback

Rather than wait until the official course evaluations at the end of the term, by which point it is too late to make a difference for your experience, please feel free to get in touch with your instructor at any point during the term with any suggestion about any aspect of the course. In particular, do not hesitate to let us know if there are aspects of the course that you particularly like, so that we can keep them that way, or if there are specific aspects that are challenging, so that we can provide more help before it is too late. This naturally does not apply to the technical content of the course (the syllabus) which is fixed. The course is an elective and designed to appeal to those who are interested in this particular topic.