Advanced Topics in Applied Systemtheory (KV)


Sommer Semester 2007

Armin Biere, Toni Jussila


Presentation schedule:

19.6.2007 Praxmarer, Lichtberger, Neuer, Hochrieser
26.6.2007 Schwaighofer, Vida, Zwirchmayr

Primer on presentations.

Threading slides, deadlock.c, and debugdeadlock.c.

Profiling slides available here.

Memory debugging slides available here.

Symbolic debugging slides available here.

Source code for the test case (debugged on April 17) with ebddres available here.

QBF and SMV slides available here.

Set of test QBF formulas available here.

First Meeting is on March 13.

Project Assignments

Delta Debuggers

Programmer Target Language Implementation Language
Peter Praxmarer QBF C++
Wilhelm Lichtberger QBF C
Hanno Neuer QBF Java

Paper Presentations

Presenter Topic Slides
Arnold Schwaighofer Paper 1 slides
Marlene Hochrieser Paper 9 slides
Andreas Vida Paper 7 slides
Jakob Zwirchmayr Paper 5 slides


In order to pass the course, you are required to take part in the lectures and present a project. The project is either a small programming assignment or presentation of a scientific publication. Precise project assignments below.


We meet regularly on Tuesday from 17:15 to 18:45 in room T211.

13.3.2007 Testing
20.3.2007 Delta Debugging
27.3.2007 SMV and QBF
17.4.2007 Symbolic Debugging
24.4.2007 Memory Debugging
8.5.2007 Profiling
22.5.2007 Thread Debugging
5.6.2007 Project Presentation I
12.6.2007 Project Presentation II
19.6.2007 Project Presentation III
26.6.2007 Project Presentation IV


Programming exercises

The programming assignment is to write a delta debugger for either the SMV of QBF file format. SMV is a model checker input language and QBF stands for Quanfitied Boolean Formula. Both formats are presented in sufficient detail on 27.3.2007.

You can freely choose the programming language you implement the debugger in (unless someone else has already chosen it).

Paper presentations

Below is a list of papers / links that can be chosen for presentation followed by the chapter of the book to which the material relates. The book chapter can and should be used as supporting material.
  1. Claessen, K. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, (Book chapter 5,13)
  2. Tip, F. A survey of program slicing techniques. Journal of programming languages 3(3), (Book chapter 7)
  3. Chelf, B. Squashing bugs at the source, Linux Magazine 55, (Book chapter 7)
  4. Zhang, X. and Gupta, R. Cost-effective Dynamic program slicing, (Book chapter 9)
  5. Design by contract: Eiffel, (Book chapter 10)
  6. Z Programming language, (Book chapter 10)
  7. SPEC#, (Book chapter 10)
  8. Ernst, M.D. et al. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions of Software Engineering, (Daikon project, presented in detail in book chapter 11)
  9. Choi J.-D., and Zeller A. Isolating failure-inducing thread schedules, Proceerings of the international symposium on software testing and analysis (ISSTA), (Book chapter 13)
  10. Zimmermann, T. and Zeller A. Visualizing Memory Graphs, Proceedings of the international Dagstuhl seminar on software visualization (LNCS 2269), (Book chapter 14)
  11. They write the right stuff, (Book chapter 15)


Why Programs fail. A guide to systematic debugging. Andreas Zeller. Morgan Kaufmann, 2005.

Table of contents available from Amazon.

Jerry J. Harrow: Runtime Checking of Multithreaded Applications with Visual Threads.

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson: Eraser: A Dynamic Data Race Detector for Multithreaded Programs.