JKU / TNF / INF
[ news | requirements | schedule | Projects | Links ]
||Praxmarer, Lichtberger, Neuer, Hochrieser
||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.
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
||SMV and QBF
||Project Presentation I
||Project Presentation II
||Project Presentation III
||Project Presentation IV
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).
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
- Claessen, K. QuickCheck: A Lightweight Tool for Random Testing
of Haskell Programs, (Book chapter 5,13)
- Tip, F. A survey of program slicing techniques. Journal of
programming languages 3(3), (Book chapter 7)
- Chelf, B. Squashing bugs at the source, Linux Magazine 55,
(Book chapter 7)
- Zhang, X. and Gupta, R. Cost-effective Dynamic program slicing,
(Book chapter 9)
- Design by contract: Eiffel,
(Book chapter 10)
- Z Programming language, (Book chapter 10)
(Book chapter 10)
- 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
- 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)
- Zimmermann, T. and Zeller A. Visualizing Memory Graphs,
Proceedings of the international Dagstuhl seminar on software
visualization (LNCS 2269), (Book chapter 14)
- 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
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.