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 (18.07.2014). Talks have to be in English, and have to fit in a 20 minute time slot + 10 minutes discussion time.
• Each student should have at least 2 meetings with the supervisor. One by mid May, and one 2 weeks before the talk (late June).
• 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:

• May 16: Discuss the conception of your paper with the supervisor.
• June 20: Submit the final version of your complete seminar paper.
• June 27: Discuss the conception of your presentation slides with the supervisor.
• July 18: Submit the final version of your complete presentation slides.

Contact information: 

• Tianhai Liu (liu@ira.uka.de)
• Carsten Sinz (carsten.sinz@kit.edu)
• Mana Taghdiri (mana.taghdiri@kit.edu)

Readings:

• A technique for finding bugs in programs automatically, to replace testing, using SAT solvers. Reading: Y. Xie and A. Aiken: Saturn: A Scalable Framework for Error Detection using Boolean Satisfiability
• An approach for debugging code and finding where the bug is. Reading: Andreas Zeller: Yesterday, my program worked. Today, it does not. Why?
• A technique for detecting information leak and security problems in software. Reading: Mana Taghdiri, Gregor Snelting, Carsten Sinz: Information Flow Analysis via Path Condition Refinement
• Ideas for mixing imperative and declarative programs, and how an interpreter may look like. Reading: Derek Rayside, Aleksandar Milicevic, Kuat Yessenov, Greg Dennis, Daniel Jackson: Agile specifications
• 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
• 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
  
• Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik: From under-approximations to over-approximations and back
• 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