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.

Topics include:

• 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

Notes:

• 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 (14.02.2014). 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 by mid Decembe, and one 2 weeks before the talk (late January).
• 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.

Deadlines:

• December 17: Discuss the conception of your paper with the supervisor.
• January 14: Submit the final version of your complete seminar paper.
• January 28: Discuss the conception of your presentation slides with the supervisor.
• February 10: Submit the final version of your complete presentation slides.

Contact information: 

• Aboubakr Achraf El Ghazi (elghazi@kit.edu)
• Stephan Falke (falke@iti.uka.de)
• Carsten Sinz (carsten.sinz@kit.edu)
• Mana Taghdiri (mana.taghdiri@kit.edu)

Readings:

• 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
• Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik: From under-approximations to over-approximations and back
• Daniel Kroening, Matt Lewis, Georg Weissenbacher: Under-approximating loops in C programs for fast counterexample detection
• Will Dietz, Peng Li, John Regehr, Vikram Adve: Understanding integer overflow in C/C++
• Isil Dillig, Thomas Dillig, Alex Aiken: Automated error diagnosis using abductive inference
• Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett: Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Andrew Reynolds, Cesare Tinelli ,Amit Goel, Sava Krstic: Finite Model Finding in SMT