Testing, Verification and Everything in Between
Seminar – Summer 2012
Universität des Saarlandes – Informatik
Campus E1 1
66123 Saarbrücken
E-mail: testingverification2012-staff@st.cs.uni-saarland.de
Telefon: +49 681 302-70970
About this Seminar
Testing is a powerful and widely used technique for software quality assurance, which is known to require significant resources in most software development projects. Testing is useful for showing the presence of bugs, not the absence of them.
On the contrary, full-functional Verification aims at proving both actual and expected software behaviour agree. It can achieve very high confidence, but it requires a lot of user expertise and resources.
In this seminar we will focus on the middle ground between these two approaches. In other words, how different techniques and tools arise from merging verification and testing (concolic testing, bounded model checking, exhaustive testing, etc.)
Place and Time
- Kick-Off meeting: Tuesday 17th April 17:00, Campus E 1 1 Room 1.09
- Weekly meeting: every Monday 9:00 a.m., Campus E 1.1. Room 1.09
- Summary hand-in: every Friday 12:00 a.m. (noon)
Important Dates
- Friday 5th October: Hand-in of annotated slides
- Friday 28th September: Final Presentations
- Monday 16th July: Deadline of doodle for the final presentation LINK
- Monday 11h June: Next meeting after the Pentecost holiday break
- Monday 11h June: Next meeting after the Pentecost holiday break
- Monday 23th April: First regular meeting
- Tuesday 17th April: End of Pre-Registration, Kick-off Session
Final Presentation Schedule
The final presentations will take place on 28th of September starting at 9 a.m. sharp.- 9:00 – 9:30: Higher-order test generation
- Patrice Godefroid (PLDI 2011)
- Assigned to: Arif
- 9:30 – 10:00: HAMPI: A Solver For String Constraints
- Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst (ISSTA 2009)
- Assigned to: Amrullokhuja
- 10:00 – 10:30: Pex - White Box Test Generation for .NET
- Nikolai Tillmann, Jonathan de Halleux (TAP 2008)
- Assigned to: Florian B.
- 11:00 – 11:30: Generating Parameterized Unit Tests
- Gordon Fraser, Andreas Zeller (ISSTA 2011)
- Assigned to: Bayram
- 11:30 – 12:00: Reducing the cost of model-based testing through test case diversity
- Hemmati, Arcuri, Briand (ICTSS 2010)
- Assigned to: Max
- 12:00 – 12:30:Systematic Testing of Database Engines Using a Relational Constraint Solver
- Shadi Abdul Khalek, Sarfraz Khurshid (ICST 2011)
- Assigned to: Alexander
- 12:30 – 13:00: Clousot: Static Contract Checking with Abstract Interpretation
- Manuel Fähndrich, Francesco Logozzo (FoVeOOS 2010)
- Assigned to: Pascal
- 14:00 – 14:30: Bounded Verification of Voting Software
- Greg Dennis, Kuat Yessenov, Daniel Jackson (VSTTE'08)
- Assigned to: Akmal
- 14:30 – 15:00: Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analysis
- Jason Belt, Robby, Xianghua Deng. (FSE 2009)
- Assigned to: Sascha
- 15:00 – 15:30: On test repair using symbolic execution
- Brett Daniel, Tihomir Gvero, Darko Marinov (ISSTA 2010)
- Assigned to: Vitali
- 16:00 – 16:30: Constraint-Based Program Debugging Using Data Structure Repair
- Muhammad Zubair Malik, Junaid Haroon Siddiqui, Sarfraz Khurshid (ICST 2011)
- Assigned to: Florian H.
- 16:30 – 17:00: Sound Empirical Evidence in Software Testing
- Gordon Fraser and Andrea Arcuri. In the ACM/IEEE International Conference on Software Engineering (ICSE), 2012
- Assigned to: Nicolas
30 minute break
60 minute break
30 minute break
Paperlist
Due to- 23th April
- Reducing the cost of model-based testing through test case diversity
- Hemmati, Arcuri, Briand (ICTSS 2010)
- Generating Parameterized Unit Tests
- Gordon Fraser, Andreas Zeller (ISSTA 2011)
- Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analysis
- Jason Belt, Robby, Xianghua Deng. (FSE 2009).
- Bounded Verification of Voting Software
- Greg Dennis, Kuat Yessenov, Daniel Jackson (VSTTE'08)
- On test repair using symbolic execution
- Brett Daniel, Tihomir Gvero, Darko Marinov (ISSTA 2010).
- Constraint-Based Program Debugging Using Data Structure Repair
- Muhammad Zubair Malik, Junaid Haroon Siddiqui, Sarfraz Khurshid (ICST 2011).
Requirements for successful participation
- Important: You can only take part in this seminar after you have successfully registered for it.
- Prerequisites: This seminar is suitable for all students, bachelor's or master's, who are interested in software engineering and its applications. You don't need to have any prior knowledge regarding the subject, however participation in any other course offered by the Software Engineering chair might be useful.
- For each meeting:
- Hand in the weekly summary one day before the meeting at 17:00. Send a PDF by mail to testingverification2012-staff@st.cs.uni-saarland.de, include your student id.
Your summary should give a good overview of the material that will be discussed in the following session.
It is intended to show us that you familiarized yourself with the material. Explicitly answer the following questions in 1-2 sentences:- What is the motivation of the approach?
- What is the contribution of the paper?
- How convincing was the evaluation technique?
- Do you consider reproducing the results is possible?
- You should also include ~3 questions on the material to prepare yourself for the discussion.
- On each session we will ask one student to kick-start the discussion based on their summary (~5 minutes). This is an opportunity for you to get early feedback on your presentation style.
- We also offer (ungraded) opportunities to present your summary in form of a five-minute presentation, allowing you to get early feedback on your presentation style.
- Grading: Your final grade will consist of the following components:
- 40 % based on your final presentation
- 20 % based on the annotated slides
- 40 % based on participation in discussions / handed-in summaries / hands-on projects