11:30-2:50PM, Monday and Friday, E7 5343
By request
Prof. Arie Gurfinkel, first . last AT uwaterloo.ca, Office Hours: by appointment online
TBA
No required textbook. Lecture slides, lecture notes, and reading material will be provided.
This course will provide an introduction to software testing and quality assurance techniques. The students will learn a wide spectrum of techniques and tools that can be used to improve and evaluate software quality ranging from mature testing methodologies to cutting edge automated verification algorithms. Topics to be covered include: coverage criteria (graph, data-flow, and logic coverage), symbolic execution (static, dynamic, concolic), constraint solving (SMT), inductive invariants, automatic deductive verification, automatic invariant synthesis, and Software Model Checking.
The course will include programming assignments in Java/C/Python. Background in Compilers and Logic is useful, but is not required.
Grades may be curved or adjusted at instructor’s discretion.
All assignments that are submitted online will be returned online.
Final exam will be in-person.
You must pass the written test and pass the assignments to pass the course. The final grade is computed using the following formula:
def grade(A, P, F):
"""Final grade calculation.
A, P, F are grades for the Assignments, the Project,
and the Final, respectively. Normalized to 100%.
"""
normal = 0.35*A + 0.5*F + 0.15*P
if F >= 50 and A >= 50:
return normal
else:
return 49There are three choices of projects. Projects can be done in groups of 2. You must declare your project by the end of Week 8. All projects must be approved by the instructor.
The exact project deliverables depend on the project chosen. All projects must include approximately a 10 page report. The length of the report depends on the amount of code involved in the project (i.e., more code means shorter report).
In the assignments, you will be implementing a symbolic execution engine and a verification engine for a small imperative language. The project is to implement additional advanced features for the language.
Implement at least two features from the list in the symbolic execution engine for wlang
Concolic execution in EXE-style.
Concolic execution in DART-style.
A different exploration strategy. Potential choices are Depth First Search, Breadth First Search, A* Search, etc.
Symbolic state merging. For example, following this post. TL;DR: symbolic states can be merged together by taking disjunction of their path conditions. Merging symbolic states reduces the number of symbolic states generated, at the expense of complicated path condition.
Use incremental solving mode of Z3. During symbolic execution many similar queries are solved over and over again. Performance of symbolic execution can be improved by using incremental solving abilities of SMT solver that allow adding (and withdrawing) constraints between multiple calls. Details on available incremental interfaces are here. There are at least two different incremental solving interfaces (Scopes and Assumptions). Using each one counts for one implementation.
Add support for bit-precise symbolic execution using the theory of bit-vectors.
Implement verification condition generation using Weakest Pre-Condition. We will cover this in class in Week 10. Here is a link to the (old) slides.
Extend wlang with functions. This requires adding functions to the parser.
We can help with that. This is a significant feature that counts for two.
Extend the language to allow for functions specifications (requires and
ensures from Dafny that we will cover in class).
Extend wlang with references. A reference is a variable that is allocated
on the heap. This requires changing the parser. We can help with that. This
is a significant feature that counts for two.
Code for the features. If the project is done in groups, request us to create a group repository for you. All code is to be submitted into the group repository (if the project is done in a group), or in your course repository (if the project is done independently)
Test cases. You have to achieve complete statement and branch coverage for all the new code that you have written.
Report. An approximately 10 page report (can be 9, can be 15, cannot be 5) describing the design decisions for your implementation, any theoretical foundations of your implementation, and your testing strategy. Report is to be submitted in PDF. Suggested style is LNCS. An Overleaf template is here. If you insist on using MS-WORD, a template is available here.
Throughout the course, we will learn of several quality assurance techniques including fuzzing, symbolic execution, and deductive verification. In this project, you have to propose a program or an algorithm to verify with one of the techniques that we have studied in the course. The complexity of the artifact being verified will depend on the verification technique involved. The more complex the verification technique the simpler the artifact being verified can be.
This project requires approval of the instructor. Talk to me. Sooner the better. Deadline is Week 10.
Code and any other artifacts you produce. If the project is done in groups, request us to create a group repository for you. All code is to be submitted into the group repository (if the project is done in a group), or in your course repository (if the project is done independently)
Report. An approximately 10 page report (can be 9, can be 15, cannot be 5) describing your experience, any theoretical foundations, any design decisions, and implementation that you had to do. Report is to be submitted in PDF. Suggested style is LNCS. An Overleaf template is here. If you insist on using MS-WORD, a template is available here.
Quality assurance and automated verification are active areas of research. In this project, you will conduct an independent study into a topic that is closely related to the material of the course but is not explicitly covered. The study must include reading at least two scientific papers. The outcome of the project can be an implementation of new technique or a report on the topic studied.
This project requires approval of the instructor. Talk to me. Sooner the better. Deadline is Week 10.
In the case of a disruption to in-person classes, the lectures will transition to an online live-stream format. If necessary, the final exam will be conducted online as well.
All other course work is already being conducted in a way that is compatible with online interaction and no change will be necessary.
This course includes the independent development and practice of specific skills, such as programming, reasoning, and application of logic. Therefore, the use of Generative artificial intelligence (GenAI) trained using large language models (LLM) or other methods to produce text, images, music, or code, like Chat GPT, DALL-E, or GitHub CoPilot, is not permitted in this class. Unauthorized use in this course, such as running course materials through GenAI or using GenAI to complete a course assessment is considered a violation of Policy 71 (plagiarism or unauthorized aids or assistance). Work produced with the assistance of AI tools does not represent the author’s original work and is therefore in violation of the fundamental values of academic integrity including honesty, trust, respect, fairness, responsibility and courage (ICAI, n.d.).
You should be prepared to show your work. To demonstrate your learning, you should keep your rough notes, including research notes, brainstorming, and drafting notes. You may be asked to submit these notes along with earlier drafts of their work, either through saved drafts or saved versions of a document. If the use of GenAI is suspected where not permitted, you may be asked to meet with your instructor or TA to provide explanations to support the submitted material as being your original work. Through this process, if you have not sufficiently supported your work, academic misconduct allegations may be brought to the Associate Dean.
In addition, you should be aware that the legal/copyright status of generative AI inputs and outputs is unclear. More information is available from the Copyright Advisory Committee: https://uwaterloo.ca/copyright-at-waterloo/teaching/generative-artificial-intelligence
Students are encouraged to reach out to campus supports if they need help with their coursework including:
By registering for this class, students agree to the following class policies:
Independent work. All work turned in will be that of the individual student unless stated otherwise. Violations would result in zero credit to all students concerned. Policy 71 will be followed for any discovered cases of plagiarism.
Lateness. You have 2 days of lateness to use on assignment submissions throughout the term. Each day you hand in an assignment late consumes one of the days of lateness. If you consume all of your late days, assignments that are still late will get 0 marks. You can only hand in an assignment up to the time all assignments are returned. Missed assignments get 0 marks. For example, you may hand in A1 two days late and A2 on time, or you can hand in A1 one day late and A2 one day late.
Missed Quizzes. If you miss a quiz, you will receive 0 marks for the quiz. If you have a legitimate reason (at the discretion of the instructor) that you cannot take quiz, and obtain permission from the instructor a week in advance, the percentage for the quiz may be shifted to the final. No alternative quiz time will be provided.
Academic Integrity. In order to maintain a culture of academic integrity, members of the University of Waterloo community are expected to promote honesty, trust, fairness, respect and responsibility. [Check http://www.uwaterloo.ca/academicintegrity for more information.]
Grievance. A student who believes that a decision affecting some aspect of his/her university life has been unfair or unreasonable may have grounds for initiating a grievance. Read Policy 70, Student Petitions and Grievances, Section 4, http://www.adm.uwaterloo.ca/infosec/Policies/policy70.htm. When in doubt please be certain to contact the departments administrative assistant who will provide further assistance.
Discipline. A student is expected to know what constitutes academic integrity [check http://www.uwaterloo.ca/academicintegrity] to avoid committing an academic offense, and to take responsibility for his/her actions. A student who is unsure whether an action constitutes an offense, or who needs help in learning how to avoid offenses (e.g., plagiarism, cheating) or about rules for group work/collaboration should seek guidance from the course instructor, academic advisor, or the undergraduate Associate Dean. For information on categories of offenses and types of penalties, students should refer to Policy 71, Student Discipline, http:://www.adm.uwaterloo.ca/infosec/Policies/policy71.htm. For typical penalties check Guidelines for the Assessment of Penalties, http://www.adm.uwaterloo.ca/infosec/guidelines/penaltyguidelines.htm.
Appeals. A decision made or penalty imposed under Policy 70 (Student Petitions and Grievances) (other than a petition) or Policy 71 (Student Discipline) may be appealed if there is a ground. A student who believes he/she has a ground for an appeal should refer to Policy 72 (Student Appeals) http://www.adm.uwaterloo.ca/infosec/Policies/policy72.htm.
Note for Students with Disabilities. The AccessAbility Services, located in Needles Hall, Room 1132, collaborates with all academic departments to arrange appropriate accommodations for students with disabilities without compromising the academic integrity of the curriculum. If you require academic accommodations to lessen the impact of your disability, please register with the AccessAbility Services at the beginning of each academic term.
University of Waterloo Territorial Acknowledgement The University of Waterloo acknowledges that much of our work takes place on the traditional territory of the Neutral, Anishinaabeg and Haudenosaunee peoples. Our main campus is situated on the Haldimand Tract, the land granted to the Six Nations that includes six miles on each side of the Grand River. Our active work toward reconciliation takes place across our campuses through research, learning, teaching, and community building, and is co-ordinated within the Office of Indigenous Relations.