Diese Seite auf Deutsch  Research Group Computer Science 2  Dept. of Computer Science RWTH

Seminar: Verification Techniques

(S2, WS 2018/19)

LuFG Informatik 2


Instructors

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



Contents

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:



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

TitleLiteratureSupervisorStudentTime
Termination Analysis for Term Rewrite Systems Using Dependency PairsLinkJera HenselHumam Kourani09:00-09:45
Termination Analysis of Integer Transition SystemsLinkDavid KorzeniewskiDamyan Dimanov09:45-10:30
Automated Termination Proofs for Java Programs with Cyclic DataLinkStefan DollaseChristian Rennert10:30-11:15
Analyzing Runtime and Size Complexity of Integer ProgramsLinkMarcel HarkPhilipp Ludwig11:15-12:00
Automated Program Verification Environment (AProVE)LinkProf. Dr. Jürgen Giesl12:00-12:15
Bounded Expectations: Resource Analysis for Probabilistic ProgramsLinkMarcel HarkVincent Wehrwein13:45-14:30
Local Reasoning about Programs that Alter Data StructuresLinkStefan DollaseValentin Promies14:30-15:15
The KeY Symbolic Execution DebuggerLinkDavid KorzeniewskiNils Lommen15:15-16:00



Templates

Area

Theoretical Computer Science



Further Details and Questions

For further details please contact Marcel Hark.


Disclaimer  Research Group Computer Science 2  Dept. of Computer Science RWTH