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 (10.02.2012). Talks will be in English, and should fit in a 30 minute time slot + 10 minutes discussion time.
• Each student should have at least 2 meetings with the supervisor. One in early December, and one 2 weeks before the talk (mid January).
• Each student should submit a write-up (10-12 pages) at the end of the semester (11.02.2012 at the latest). A short summary should be submitted at the second meeting with the supervisor.

Contact information:

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

Readings:

• Vijay Ganesh: Decision procedures for bit-vectors, arrays, and integers
• Vijay Ganesh, David L. Dill: A decision procedure for bit-vectors and arrays
• Robert Brummayer, Armin Biere: Lemmas on demand for the extensional theory of arrays
• Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar: Efficient SAT-based bounded model checking for software verification
• Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte: A precise yet efficient memory model for C
• Yeting Ge, Clark Barrett, Cesare Tinelli: Solving quantified verification conditions using satisfiability modulo theories
• Roberto Bruttomesso, Natasha Sharygina: A scalable decision procedure for fixed-width bit-vectors
• Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop summarization using abstract transformers
• Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst: HAMPI: A Solver for string constraints
• 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
• Helga Velroyen, Philipp Rümmer: Non-Termination Checking for Imperative Programs
• 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