Verification Techniques (WS 2018/19)

Research Group Computer Science 2

Dept. of Computer Science

Seminar: Verification Techniques
(S2, WS 2018/19)
LuFG Informatik 2

Instructors

Prof. Dr. Jürgen Giesl, Stefan Dollase, Marcel Hark, Jera Hensel, David Korzeniewski

Several techniques and methods for program verification will be presented in this seminar.

Times

The seminar takes place on the 6th of February 2019 in our seminar room (E2, room 4201b). Talks will be starting at 9:00. See below for the schedule. We have a series of strict deadlines before the seminar will take place:

26.10.2018: Contact your supervisor
31.10.2018: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
16.11.2018: Withdrawing without failing the seminar.
14.12.2018: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
23.01.2019: Complete slides for your talk and send them to your supervisor.
30.01.2019: Hand in final version of your seminar paper.
06.02.2019: Seminartalks

Requirements

Your seminar paper should have 10 pages and be written in either English or German. Do not provide an index or table of contents, but attach a list of references. More than 5 spelling or grammar mistakes on a single page will lead to an immediate rejection of your paper, so please use an automated spell checker!

The seminar talks should not take more than 25 minutes and can be held in English or German.

Prerequisites

Participants should have knowledge in program verification or related areas (for example "functional programming", "logic programming", "term rewriting", "satisfiability checking", "model checking", "static program analysis", "semantics and verification of software", etc.).

Topics

Title Literature Supervisor Student Time

Termination Analysis for Term Rewrite Systems Using Dependency Pairs Link Jera Hensel Humam Kourani 09:00-09:45

Termination Analysis of Integer Transition Systems Link David Korzeniewski Damyan Dimanov 09:45-10:30

Automated Termination Proofs for Java Programs with Cyclic Data Link Stefan Dollase Christian Rennert 10:30-11:15

Analyzing Runtime and Size Complexity of Integer Programs Link Marcel Hark Philipp Ludwig 11:15-12:00

Automated Program Verification Environment (AProVE) Link Prof. Dr. Jürgen Giesl 12:00-12:15

Bounded Expectations: Resource Analysis for Probabilistic Programs Link Marcel Hark Vincent Wehrwein 13:45-14:30

Local Reasoning about Programs that Alter Data Structures Link Stefan Dollase Valentin Promies 14:30-15:15

The KeY Symbolic Execution Debugger Link David Korzeniewski Nils Lommen 15:15-16:00

Title	Literature	Supervisor	Student	Time
Termination Analysis for Term Rewrite Systems Using Dependency Pairs	Link	Jera Hensel	Humam Kourani	09:00-09:45
Termination Analysis of Integer Transition Systems	Link	David Korzeniewski	Damyan Dimanov	09:45-10:30
Automated Termination Proofs for Java Programs with Cyclic Data	Link	Stefan Dollase	Christian Rennert	10:30-11:15
Analyzing Runtime and Size Complexity of Integer Programs	Link	Marcel Hark	Philipp Ludwig	11:15-12:00
Automated Program Verification Environment (AProVE)	Link	Prof. Dr. Jürgen Giesl		12:00-12:15
Bounded Expectations: Resource Analysis for Probabilistic Programs	Link	Marcel Hark	Vincent Wehrwein	13:45-14:30
Local Reasoning about Programs that Alter Data Structures	Link	Stefan Dollase	Valentin Promies	14:30-15:15
The KeY Symbolic Execution Debugger	Link	David Korzeniewski	Nils Lommen	15:15-16:00

Templates

Area

Theoretical Computer Science

Further Details and Questions

For further details please contact Marcel Hark.

Disclaimer