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 test case generation
• Automatic debugging tools
• Decision procedures for bit-vectors, arrays, and integers
• Software bounded model checking
• Feedback-driven program checking

Notes:

• First meeting will be held on Thursday, 21.10.2010, 14:00 (room 236) in which each student picks a topic of his/her own interest.
• Each student has to give a presentation on his/her chosen topic at the end of the semester (03.02. and 10.02.2011). Talks will be in English, and should fit in a 20 minutes 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 (6-10 pages) at the end of the semester (12.02.2011 at the latest). A short summary should be submitted at the second meeting with the supervisor.

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
• Chandrasekhar Boyapati, Sarfraz Khurshid and Darko Marinov: Korat: Automated Testing Based on Java Predicates
• Andreas Zeller: Yesterday, my program worked. Today, it does not. Why?