Goethe Logo

16. Jahrestagung der GI-Fachgruppe

Logik in der Informatik

Frankfurt am Main, November 6-7, 2009

The 16th annual meeting of the "GI Fachgruppe 'Logik in der Informatik'" will take place November 6-7, 2009 at Goethe University Frankfurt, organized by Manfred Schmidt-Schauß and Nicole Schweikardt.

Participants should register until 12th of October 2009 by using the registration form.
Call for Participation
The call for participation (in German) is available in ASCII format here
Participants may book their hotel directly by using their web-pages. Here are hotels we have used successfully on previous occasions for meetings.
  • The Breesen, bed & breakfast Hotel, Varrentrappstraße 73, 60486 Frankfurt am Main,
    (2 min walk to meeting location)
  • Art-Hotel Robert Mayer,Robert-Mayer-Str. 44, 60486 Frankfurt am Main,
    (5 min walk to meeting location)
  • Hotel Gölz, Beethovenstraße 44, 60325 Frankfurt am Main,
    (5 min to meeting location)
  • Hotel Atrium (***), Beethovenstraße 30, 60325 Frankfurt am Main,
    (5 min to meeting location)
  • Hotel Falk (***), Falkstraße 38A, 60487 Frankfurt am Main
    (15 min to meeting location)
  • Hotel Diana (***), Westendstraße 83, 60325 Frankfurt am Main,
    Tel.: : +49 69 9 07 44 20, Fax: +49 69 90 74 42 77
    (5 min to meeting location)
Invited Talks
  • Markus Aderhold, TU Darmstadt:
    Semi-Automated Program Verification -- Techniques and Heuristics in VeriFun
    The goal of program verification is to formally show that a given program satisfies certain properties. Verification tools help to cope with the complexity of the verification process, for instance by ensuring that there are no gaps in a proof (e.g., a missing case). In addition, verification tools can try to automatically construct (parts of) a proof. This talk gives an overview of different kinds of automation that are used in current verification tools. In particular, we describe how inductive proofs are constructed in the verifier VeriFun. We discuss challenges in the verification of programs with higher-order functions (i.e., functions that operate on functions) and show how such programs can be verified using a special form of induction schemes.
  • Martin Otto, TU Darmstadt:
    On Methods for Deciding Boundedness of Least Fixed Points
    Least fixed points provide a natural extension of more static logics like FO to capture the results of monotone relational recursion. True recursion is dynamic in the sense of being of a-priori unbounded depth, and may not be replaced by a fixed length static iteration. But the distinction between bounded and unbounded recursion is in general undecidable. The boundedness problem was first highlighted as a decision problem in connection with qurey optimisation for Datalog programs in the 80s. Only very limited cases can be decided. In the context of FO, boundedness for syntactic fragments may be regarded as a generalisation of the satisfiability problem for corresponding fragments of FO. Unsurprisingly therefore, undecidabilty abounds - and a model theoretic explanation for the rare benign cases has been a challenge. In this talk I shall survey some long-standing results and connections, intermediate developments towards new decidability results, and report on recent progress and generalisations including ongoing work with Achim Blumensath and Mark Weyer.
  • Christoph Weidenbach, MPII Saarbrücken
    Automation of Logic The Past 15 Years
    Starting from the end of the 90s the average performance of SAT solvers has increased by two orders of magnitude. Partly due to new algorithms and datastructures and due to a new calculus for SAT. This has moved the use of these tools from almost purely academic to standard industry. For example, in the context of (hardware) verification and (bounded) model checking.
    Building on the success of SAT solvers a new area of procedures evolved starting from the beginning of this century: SMT solvers, i.e., Sat Modulo Theory solvers. Here the boolean atoms of propositional logic are replaced by first-order atoms over some given theory. A combination of the overall SAT procedure together with a decision procedure for conjunctions of atoms from the theory then decides aribtrary (ground) formulas over the theory and even combinations thereof. SMT solvers have meanwhile found their way into industrial (software) verification pipelines and optimization tools.
    In parallel to the SAT based development the combination of theories with and within first-order logic has gained serious attention. It resulted in the development of new decision procedures and (weakly) complete calculi for even fragments of second-order logic.
Prospective Participants
  • Isolde Adler, Goethe-Universität Frankfurt am Main
  • Frederik Harwath, Goethe-Universität Frankfurt am Main
  • André Hernich, Goethe-Universität Frankfurt am Main
  • Martin Hofmann, LMU München:
    Pure Pointer Programs and Logspace
  • Ahmet Kara, TU Dortmund:
    On the Hybrid Extension of CTL and CTL+ [ Abstract: show abstract hide abstract]
  • Markus Krötzsch, Karlsruhe Institute of Technology
    When Ontologies Meet Rules: Integrating Description Logics and Horn Logic
  • Jiamou Liu, Universität Leipzig:
    The Isomorphism Problem on Classes of Automatic Structures [ Abstract show abstract hide abstract]
  • Markus Lohrey, Universität Leipzig
  • Conrad Rau, Goethe-Universität Frankfurt am Main
  • Sebastian Rudolph, Karlsruhe Institute of Technology:
    Decidability of Conjunctive Queries in Description Logics with Inverses, Counting and Nominals
  • David Sabel, Goethe-Universität Frankfurt am Main:
    Proof Methods for Polymorphically Typed Contextual Equivalence [ Abstract: show abstract hide abstract]
  • Manfred Schmidt-Schauß, Goethe-Universität Frankfurt am Main:
    Reconstruction of a Logic for Functional Programs
  • Peter H. Schmitt, Universität Karlsruhe
  • Nicole Schweikardt, Goethe-Universität Frankfurt am Main:
    Addition-invariant first order and regular languages
  • Thomas Schwentick, TU Dortmund
  • Jan Schwinghammer, Universität des Saarlandes:
    Nested Hoare Triples and Frame Rules for Higher-order Store
  • Helmut Seidl, TU München
  • Christoph Walther, TU Darmstadt


10:30-11:25Christoph Weidenbach
11:25-11:50Martin Hofmann
11:50-12:15Jan Schwinghammer
14:00-14:55Martin Otto
14:55-15:20Nicole Schweikardt
15:50-16:15Jiamou Liu
16:15-16:40Sebastian Rudolph
16:40-17:05Markus Krötzsch
18:30 Dinner / Abendessen


09:15-10:10Markus Aderhold
10:40-11:05David Sabel
11:05-11:30Ahmet Kara
11:30-11:55Manfred Schmidt-Schauß
The department of Computer Science is located at Robert-Mayer-Str. 11-15 on Campus Bockenheim, near the tram station "Varrentrappstr." (trams no. 16, 17) or the subway station "Bockenheimer Warte" (trains U4,U6,U7). A map can be found here. The location of the building can be found here.
  • By Air (Frankfurt Airport): There are two possiblities:
    • A taxi from Frankfurt Airport takes about 20 minutes to the university and costs about 30 EURO.
    • A cheaper way (about 4 EURO from the travel center (Reisezentrum) ticket counter or from vending machines) is to catch S8 or S9 train from "Gleis" 1 of the "Regionalbahnhof" under Terminal 1 to Frankfurt Hauptbahnhof (Main Train Station). There change to subway line U4 in the direction Messe / Bockenheimer Warte (your ticket is also valid for the subway). Leave the subway at "Bockenheimer Warte".
  • By Air (Frankfurt-Hahn Airport): The cheapest way is to take a bus from Frankfurt-Hahn airport to Frankfurt Hauptbahnhof (Main Train Station) (the ticket costs 12 EUR). The bus takes about 1:45h. From Frankfurt Hauptbahnhof (Main Train Station) you can walk to the university in about 25 minutes, or otherwise change to subway line U4 in the direction Messe / Bockenheimer Warte. You may have to buy a ticket from a vending machine. Get off at "Bockenheimer Warte".
  • By Train: If you arrive by train at Frankfurt Hauptbahnhof (Main Train Station) you can walk to the university in about 25 minutes, or otherwise change to subway line U4 in the direction Messe / Bockenheimer Warte. You may have to buy a ticket from a vending machine. Get off at "Bockenheimer Warte".
  • By Car: We strongly advise you not to take a car because parking space is limited in Frankfurt and especially around the university. You may use the parking area next to the Bockenheimer Depot (very short footwalk, see map).
    • Arriving from the north via Autobahn A5: get off the Autobahn at Nordwestkreuz Frankfurt in direction of Miquelallee (Bockenheim/Hauptbahnhof/Messe) and stay on the Miquelallee until you reach a major crossing and traffic lights. Turn right and right again at the Bockenheimer Depot to enter the parking area.
    • Arriving from the west, east and south via Autobahn A3 or A5: follow the A5 north of Frankfurter Kreuz (the intersection of the A3 and A5 at Frankfurt airport) in the direction of Kassel or Westkreuz Frankfurt (Frankfurt-West). Get off at Westkreuz Frankfurt exit in direction F-Stadmitte/ Universität/ Congress C. Use the left lanes on this road. Stay on this until you see the Messeturm (Messe Tower on the map) with the hammering geologist statue in front of it. At the roundabout, go nearly 270° around and turn right into the Senckenberganlage. Stay on this road until you will have passed the Senckenberg Museum with the dinosaur in front of it (on your left hand side). Pass two sets of traffic lights and immediately move to the very left lane. There, after the third set of traffic lights, you have the possibility for a U-turn. Move to the right lane and turn right after about 50m at the traffic lights. Turn right again at the next traffic lights and enter the Bockenheimer Depot parking area.
Some links:
Further Information
(c) 2009 KIST, Impressum, Last modified: $Author: sabel $, $Date: 2009/11/09 12:55:09 $
Valid XHTML 1.0 Transitional Valid CSS!