LARA

Software Analysis and Verification (March-June 2007 Class)

This class is taught next in Spring 2008.

Tools for automated analysis and verification of software can greately improve reliability of software that we use every day. The underlying techniques are also used for compiler optimizations and program understanding. In recent years, new algorithms and combinations of existing techniques have made such tools more effective than in the past. This course gives an overview of basic techniques, as well as the recent advances that made this progress possible.

Projects

Here are the SAV07 Projects completed by students in the second half of the semester. Projects are one of the key components of this course.

Homeworks

Homeworks (assigned approximately every two weeks in the first half of the semester):

Resources

Here is an editable SAV07 Resource page.

Lectures

These are lecture notes, developed by the instructor as well as by the students based on their notes during the class.

See also Tresor seminar for relevant talks in this area.

  • Friday, 2007-06-29, 23:59: email your final projects to the instructor in electronic form (both the paper write-up and any software developed)

Announcements

General Information

Grading is based on final project (both the presentation and the writeup), homeworks, taking lecture notes, summaries of papers discussed, and class participation. There are be no written exams, finals, midterms, or any quizes that affect the grade.

Instructor: Viktor Kuncak.

Schedule:

  • Wednesday, 11:15-12:45 (no break), BC01 C, Office hours with instructor: by appointment
  • Thursday, 14:15-12:45, BC01 C (exception: BC02 for the first two weeks)
  • Thursday, 16:15-18:00, BC01 T (exception: BC02 for the first two weeks)

Here is the preliminary quiz that was emailed at the start of the class. Please read answers to selected quiz questions.

Structure of the class:

  • Both lectures and exercises are presented by Viktor Kuncak. Both lectures and exercises are equally important. Generally, lectures are in lecture slots and exercises in exercise slots, but there may well be exceptions.
  • Student attendance is not formally verified, but active class participation is an important component of the grade.
  • The following is the format of activities:
    • Lectures: the topic and suggested reading are announced ahead of time. Active participation is strongly encouraged. For each lecture (except the first week), one or two students are assigned a task of “scribing”, that is, writing down lecture notes and entering them into a course wiki in a format.
    • Homeworks: homeworks are assigned on exercises each Thursday and are due in paper form (for theoretical part) and electronic form (for implementation part), by the start of the class on next Thursday, unless otherwise stated. Each exercise starts with the discussion and initial grading of the previous week's homework. We then continue with the new discussion and preparation for the next homework.
    • Paper discussions: Some of the classes involve paper discussions. In that case, the homework for the class is to write a critical summary of the paper to be discussed.
    • In the second half of the semester, there will be no implementation homework. Instead, students work on their project. Please discuss the topic of your possible projects as early as possible. In the last weeks, students present their projects in the class and hand in a 5 page paper on their project.

The original class description.