In this seminar, we introduce some state-of-the-art techniques that help programmers check the correctness of their developed software systems. Examples of correctness properties include: the program does not crash (eg, through null pointer exceptions), it does not contain security vulnerabilities (such as buffer overflows), and it calculates the correct result. We focus on lightweight techniques that are fully automatic, easy-to-use, and do not require much user-provided assistance, and thus present a potential to be applied to real-world industrial software.
- Automatic debugging tools
- Non-termination detection
- Decision procedures for bit-vectors, arrays, and integers
- Software bounded model checking
- Feedback-driven program checking
- Information flow analysis
- There is no official first class for this seminar. The students can join any time they like, but they are responsible for preparing their presentations and written reports according to the timeline explained below.
- Interested students must pick a topic from the following list and inform the lecturers by email. The corresponding lecturer will then set up a meeting with the student to discuss the topic further.
- Each student has to give a presentation on his/her chosen topic at the end of the semester (19.07.2013). Talks have to be in English, and have to fit in a 30 minute time slot + 10 minutes discussion time.
- Each student should have at least 2 meetings with the supervisor. One in the end of May, and one 2 weeks before the talk (early July).
- Each student has to submit a seminar paper (10-12 pages, LaTeX using LNCS style). Use a spell-checker and carefully proofread your paper before submitting any version to your supervisor. If there are more than five mistakes on a single page, the review of your paper will be aborted and it will be returned to you immediately.
- May 27: Discuss the conception of your paper with the supervisor.
- June 24: Submit the final version of your complete seminar paper.
- July 8: Discuss the conception of your presentation slides with the supervisor.
- July 15: Submit the final version of your complete presentation slides.
- Tianhai Liu (firstname.lastname@example.org)
- Stephan Falke (email@example.com)
- Carsten Sinz (firstname.lastname@example.org)
- Mana Taghdiri (email@example.com)
- Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop summarization using abstract transformers
- T. Ball, S. K. Rajamani: Automatically Validating Temporal Safety Properties of Interfaces
- Y. Xie and A. Aiken: Saturn: A Scalable Framework for Error Detection using Boolean Satisfiability
- Andreas Podelski, Andrey Rybalchenko: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement
- Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies: Abstraction Refinement for Quantified Array Assertions
- Sarfraz Khurshid, Corina Pasareanu, Willem Visser: Generalized Symbolic Execution for Model Checking and Testing
- Andreas Zeller: Yesterday, my program worked. Today, it does not. Why?
- Ashutosh Gupta, Thomas Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu: Proving Non-Termination
- Jacob Burnim, Nicholas Jalbert, Christos Stergiou, Koushik Sen: Looper: Lightweight Detection of Infinite Loops at Runtime
- Mana Taghdiri, Gregor Snelting, Carsten Sinz: Information Flow Analysis via Path Condition Refinement