Master Seminar: Selected Topics in Software Analysis
Software Analysis is concerned with automatically determining properties of programs, e.g. the absence of bugs or the validity of assertions. In this seminar, we take a look at some selected approaches to software analysis, thereby complementing the contents of the course “Software Analysis”.
Application:
For taking part in this seminar, you need to apply to it in written form (by email). For this, take a look at the below given seminar topics. Choose one of these topics (the one which you would preferably like to present in the seminar). Write a half-page statement on why you are interested in the topic of the seminar in general and in your chosen topic in particular. Send this together with your name and student id (Matrikelnummer) to Arnab Sharma (arnab.sharma@uni-paderborn.de) by March 30th, 2018. We will then select the participants on the basis of these statements. We will most likely have more applications than places, thus participation cannot be guaranteed.
Prerequisite:
Successful participation in class “Software Analysis” or “Model Checking” (successful = exam passed).
Organizational issues:
Language: The language of the seminar is English, i.e. you will need to give your presentation in English as well as write your report in English.
Important Dates:
Preliminary meeting: 17th April, 2018, 05.00 pm, O4.267
Submission of the first version of the slides: 27th May, 2018 till 11.59.00 pm
Your presentation: 11th - 13th June, 2018, 04.00 pm to 06.30 pm
Submission of the first version of the summary report: 1st July, 2018 till 11.59.00 pm
Submission of the review report: 13th July, 2018 till 11.59.00 pm
Submission of the final version of the summary report: 20th July, 2018 till 11.59.00 pm
Your submissions of slides, reports etc. will have to be handed in via the Koala system.
Questions: Questions regarding the seminar are answered by Arnab Sharma (english only).
Requirements for passing the seminar
- give a ca. 30-minute talk and prepare for a follow up discussion
- written report (ca. 9 pages)
- active participation in the discussion
- adhere to the dates and appointments
- review reports of two other participants
Before the talk, there should have been at least two meetings with your supervisor. More information on this will be given in the preliminary meeting.
Topics and articles:
1. Stateless Modelchecking: Patrice Godefroid. Model Checking for Programming Languages using VeriSoft. In POPL 1997, ACM.
2. Conditional Model Checking: Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, Philipp Wendler: Conditional model checking: a technique to pass information between verifiers. SIGSOFT FSE 2012: 57
3. Symbolic Execution:
- Cristian Cadar, Koushik Sen: Symbolic execution for software testing: three decades later. Commun. ACM 56(2): 82-90 (2013)
- James C. King: Symbolic Execution and Program Testing. Commun. ACM 19(7): 385-394 (1976)
4. Shape Analysis: Mooly Sagiv, Thomas Reps, Reinhard Wilhelm (May 2002): Parametric shape analysis via 3-valued logic. ACM Transaction on Programming Languages and Systems. ACM. 24(3): 217-298
5. Data race detection: Dawson R. Engler, Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003: 237-252
6. Gordon Fraser, Andreas Zeller : Generating parameterized unit tests. ISSTA 2011: 364-374
7. Probabilistic symbolic execution: Jaco Geldenhuys, Matthew B. Dwyer, Willem Visser: Probabilistic symbolic execution. ISSTA 2012: 166-176
8. Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller: Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking.
