Zur Webseite der Informatik

Ausgewählte Themen der Softwaretechnik

“Selected Topics in Software Engineering: Software Verification”


  • 16.12.2013: The presentation schedule has been updated. See presentation section below for more details.
  • 16.07.2013: The first meeting will take place on Tuesday, 15.10.2013, 11:30-13:00 in Room 0.124. All students are required to attend for topic selection.


Software verification is the branch of Software Engineering concerned with the assurance of requirements satisfaction. With the increasing pervasiveness of software in business- and safety-critical applications, verification is gaining considerable importance. Examples of its applications are online banking, e-commerce, online booking and reservation, car and airplane control systems, remote surgery, high availability systems, such as e-mail servers, or adaptive systems, such as cloud computing controllers.

A broad range of techniques is involved in verification. Among the others, this seminar will concern:

  • Systematic testing: methodologies for automatic test case generation, including model-based testing, random testing, mutation testing, search-based techniques, non-functional testing
  • Software analysis: Floyd-Hoare axiomatic semantics, symbolic execution, abstract interpretation, anti-patterns detection
  • Formal verification: software model-checking, probabilistic model-checking, theorem proving, assume-guarantee reasoning

In this seminar, we will explore the research field of software verification including an overview of the previously mentioned topics as well as detailed discussions of selected approaches and underlying analysis principles.

Bachelor's Students attending this seminar should have an interest in critical systems design and formal methods, as well as basic notions on logics, probability, testing, and object-oriented programming.

Important dates

First meeting 15.10.2013, 11:30-13:00, Room 0.124
Paper structure and list of references* 08.11.2013
Pre-submission* 13.12.2013
Final submission* 10.01.2014
Peer-Review reports* 24.01.2014
Revised paper* 07.02.2014

See presentation section below
for a detailed schedule

*= The document (in PDF format) needs to be submitted via the seminar submission site: https://www.easychair.org/conferences/?conf=rsssvw2013. It is possible to submit supplementary materials (e.g., source code, data) as a zip file along with the paper submission.

List of topics

A complete list of topics will be presented on the first meeting. All students are required to attend for topic selection.





1 Symbolic Execution Eugen Massini *
2 Reliability Estimation under No Failure Testing Eugen Massini N.N.
3 Automatic Support for Regression Testing
Lars Grunske *
4 Complex Event Processing for Failure Detection Lars Grunske N.N.
5 Bayesian Inference using Data Flow Analysis Lars Grunske N.N.
6 Regression Testing vs. Interaction Errors Lars Grunske N.N.
7 Automatic Verification by Abstraction Sinem Getir N.N.
Compositional verification Sinem Getir N.N.
Run-time verification Sinem Getir *
10 Software Architecture/Design Verification and Essential Properties Sinem Getir *
11 Mining Specifications: Learning Specifications from Software Verification Sinem Getir N.N.
12 Model-Driven Testing with the UML Testing Profile André van HoornSinem Getir *
13 Performance Regression Testing André van HoornSinem Getir N.N.
14 Event Log Analysis Teerat Pitakrat *
15 Reliability-driven dynamic binding through fuzzy control Antonio Filieri N.N.
16 Quantitative multi-objective probabilistic model checking Antonio Filieri *
17 State-space reduction for probabilistic model-checking Antonio Filieri N.N.
18 Statistical model checking of non-deterministic programs Antonio Filieri N.N.

Presentation schedule

Room: 0.124
Time: 11:30-13:00
(*= name omitted for privacy reasons)


Presentation Date




28.01.2014 Model-Driven Testing with the UML Testing Profile André van Hoorn *
2 28.01.2014 Event Log Analysis Teerat Pitakrat *
3 04.02.2014 Symbolic Execution Eugen Massini *
4 04.02.2014 Software Architecture/Design Verification and Essential Properties Sinem Getir *
5 04.02.2014 Quantitative multi-objective probabilistic model checking Antonio Filieri *

Seminar guideline

Paper format
  • Seminar papers must be written in English and should not exceed 15 pages using the seminar LaTeX template format.
Review process
  • Each student reviews and writes review reports for 2 seminar papers of other students.
  • The review reports should comply with the review guideline (to be provided).
Revising paper
  • The students should revise their own paper based on the comments given by the supervisors and the reviewers.
  • A response to the review reports should be provided according to the response template and submitted along with the revised version of the paper.
  • The presentation should be 20 minutes long followed by 5 minutes for questions/discussion.
  • The students are encouraged to give presentations in English.


Additional information

Prof. Dr. Lars Grunske, grunske@informatik.uni-stuttgart.de
Reliable Software Systems (RSS) Group
Institute for Software Technology (ISTE), University of Stuttgart