Advanced Topic in Model-Checking, SS 2007

Instructors

• Prof. Dr. Andreas Podelski
• Alexander Malkis

Description

Software Model Checking deals with automated verification of programs. A variety of successful tools have emerged in the recent years, some of them have found application in the industry. We are going to learn about Software Model Checking: read papers about underlying methods and algorithms, play with tools, discuss in the class, find out what could be done better.

Registration

Good students are always welcome.

Topic list

includes, but is not limited to the given set of articles. To get a topic please talk to Alexander. Teams are welcome, people are allowed to share a topic.

Talk

All the speakers are supposed to give a talk in English. The format of the slides does not matter as long as it can be presented on a standard Windows or Linux machine. We advise ps/pdf (or overhead slides). For a seminar talk, the talk length is one hour plus at most 15 minutes for questions and comments from the listeners. Please send your slides to Alexander till the 24th of June 2007 so that we could look through all of them in advance. For a CAV 2007 talk, each speaker has at most 25 minutes, including discussion.

List of Participants

Students, who give a seminar talk and want to receive a certificate for it

Justus Bisser, Juergen Christ, Kais Haddadin, Matthias Heizmann, Abel F. L. Kla, Marco Muniz, Arend von Reinerdorff, Alexander Schimpf, Peter Schmitt

Students, who give a CAV 2007 talk

Daniel Dietsch, Sergio A. Feo, Matthias Heizmann, Nicola Sheldrick

Others

Stefan Arlt, Jochen Hoenicke, Alexander Malkis, Stefan Maus, Martin Mehlmann, Corina Mitrohin, Andreas Podelski (without a talk), Martin Schäf, Nassim Seghir, Martin Wehrle

Preliminary program

Submitted report

The length and the contents depend on the chosen topic. The students will be given at least two weeks after the seminar to prepare the report. We strongly encourage submissions in English. A submission in German is possible only as an exception; in this case it should be absolutely flawless. We encourage flawless submissions anyway.

We advise typing in using the "llncs" style for latex (for the LNCS author instructions see http://www.springer.de/comp/lncs/authors.html , click on "Information for LNCS Authors", download and unzip llncs2e.zip and follow the typesetting instructions from the file llncsdoc.pdf) and also advise submitting files in the ps/pdf format. Using llncs and pdf/ps format for submission is an advice, not a requirement.

Costs

The participants don't have to pay for accomodation and usual meals, but they have to pay for the extra beverages they buy there themselves. The money for these beverages will be collected at the end of the stay, so please take enough small change with you. The SWT people should fill in the application forms before the 10th of July 2007 in any case.

Remember

• You need slippers. They won't let you into the house if you have your outdoor shoes on.
• There is neither soap nor towels for all, take your own towel and your own piece of soap.
• No dogs.
• For a possible excursion you need waterproof cloths and boots and at least a liter of water.
• The speakers should take their laptop with cable AND send their slides to us as soon as they are ready.
• The speakers should think about how and how long they could still give a talk in case of a technical failure.
• Assume that it's not possible to use Internet and mobile phones at Schauinsland.
• You will have a beamer, a flipchart and an overhead projector at your disposal, but no blackboard or whiteboard.
• If you want vegetarian meals, please tell us in advance.
• It is forbidden to bring your own beverages to Schauinsland.