Seminar in Computer Science

Formal Verification

Winter Semester 2009

Armin Biere, Florian Lonsing


Please schedule individual meetings with your advisors in the last week of November to present and discuss the alpha version of your slides.

We moved the talks to January 2010.


  • 20. Oct. 2009, Armin Biere, Presetation Primer
  • 24. Nov. 2009, Alpha Version
  • 17. Dec.. 2009, Beta Version
  • 12. Jan.. 2010, First Round of Talks
  • 19. Jan.. 2010, Second Round of Talks


The selection of topics is finished, which were among the chapters of the handbook. Chapter 1, 3, 4, and 14 were not eligible, since they are part of the advanced model checking course.


  • Harald Seltner, chapters 23 and 24 on QBF, advisor FL
  • Zheng Bo, chapter 15 on Planning, advisor AB
  • Bernhard Scholze, chapter 26 on SMT, advisor AB
  • Sebastian Huber, chapter 16 on Software Verification, advisor FL


This seminar is about formal models and verification. This winter we focus on SAT solving, and particular will use chapters from the Handbook of Satisfiability as reading material.

The goal is to help students advance presentation skills and lead them towards being able to read, understand and explain scientific texts.

Each participant will select one of the topics presented at the first meeting and is supposed to give a talk based on the given material at one of the meetings. The students should work through their papers independently but are expected to consult their advisor if problems occur. In addition, we want to discuss both an alpha and a beta version of the slides not later than two respectively one week before the talk.

Active participation during presentations is expected. We also require a written report.

The seminar will start with a general introduction on how to do presentations. Individual feedback will be provided after each talk. The default language of the seminar is English and talks in English are particularly appreciated.