Testing, Debugging, and Verification TDA567/DIT082, LP2, HT2015

About This Course


Course Assistants

  • We have scheduled office hours to help you with questions. You can contact by e-mail to schedule a date and time:
    Mauricio Chimento chimento (a) chalmers.se - week 4 to 5
    Simon Robillard simon.robillard (a) chalmers.se - week 6 to 7


Course homepage: www.cse.chalmers.se/edu/course/TDA566

Discussion group: #. Messages posted in this group will reach all teachers. If you are not yet member of the group, you have to

  • obtain a google account, and
  • request an invitation to the group.
You can do both on the group page. Please send your person number along with a membership request. Alternatively, you can register using a "@student.chalmers.se" address. All kinds of questions (and answers) on the content of the course are welcome. (But don't post lab solutions!)


To pass the course a student must


The workload for an average student is expected to be around 200h. Evenly distributed over the 8 week course period that means around 25h/week. From these 25h/week only 6h/week are scheduled activity and 19h/week are your own responsibility.

The course has approximately two lectures and one exercise session each week. Participation in these is optional but very strongly recommended.

Course Contents

The course is about how to convince oneself that a program unit really does what it should. There are different methods for verifying programs that will be covered in this course:

  • testing (which has the purpose of finding errors in a program in a systematic way)
  • debugging (which has the purpose to systematically trace and eliminate an error)
  • proving or formal verification (reasoning about the program in order to guarantee correctness).

Verifying a program only makes sense if we can precisely specify what the program is supposed to do. Many specifications are written in natural language which might lead to imprecision and misunderstandings. In the course you will learn how to use precise methods for specifying functional requirements. Such precise specifications will then be our basis for the verification of programs. But they will also be useful to automatize the generation of test cases.

Learning Outcome

After a completed course the student should know
  • have understood the possibilities and limitations of both informal and formal techniques for the discovery, analysis, and resolution of program errors
  • be able to understand and express precise specifications of software units
  • be able to systematically discover inputs on which a program fails
  • be able to locate, analyse, and fix the error which caused the failure
  • have understood the principles of verification, and be able reason about simple programs for guaranteeing correctness.


The books listed below should be accessible as e-books via Chalmers library. Let us know if any of them are no longer available.

Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools Atze van der Ploeg, Oct 18, 2016