DFG-Graduiertenkolleg Mathematische Logik und Anwendungen

Graduiertenkolloquium WS 2007/2008

Vorträge

• 05.11.2007
  Herr Michael Schmidt
  Effiziente Evaluierung von XQuery-Anfragen über XML-Strömen Abstract
  

• 19.11.2007
  Herr Alexander Malkis
  Precise thread-modular verification Abstract
  

• 17.12.2007
  Herr Prof. Ulrich Furbach
  Hypertableaux, Gleichheit und Anwendungen Abstract
  Dieser Vortrag findet ausnahmsweise an der Fakultät für Angewandte Wissenschaften im Gebäude 101, Raum 02-016 statt.

Abstracts

• Effiziente Evaluierung von XQuery-Anfragen über XML-Strömen
  Effective buffer management is crucial for efficient in-memory and streaming XQuery processing. Whenever large documents or streams are processed, buffer management becomes the key prerequisiste to performance. We present a buffer management scheme which combines static and dynamic analysis to keep main memory consumption low. Our approach relies on a technique that we call active garbage collection and which actively purges buffers at runtime based on the current status of query evaluation. We present the results of a prototype implementation, and discuss novel implementation strategies for important subtasks of our buffer management scheme. In particular, we show that well-known string matching techniques, originally designed for keyword search in flat, are very useful to efficiently navigate in tree-structured data. Our experimental results demonstrate the significant impact of combined static and dynamic analysis on reducing both main memory consumption and running time.
  
  
  
• Precise thread-modular verification
  Thread-modular verification is a promising approach for the verification of concurrent programs. Its high efficiency is achieved by abstracting the interaction between threads. The resulting polynomial complexity (in the number of threads) has its price: many interesting concurrent programs cannot be handled due to the imprecision of the abstraction. We propose a new abstraction algorithm for thread-modular verification that offers both high degree precision and polynomial complexity. Our algorithm is based on a new abstraction domain that combines Cartesian abstraction with exception sets, which allow one to handle particular thread interactions precisely. Our experimental results demonstrate the practical applicability of the algorithm.
  
  
  
• Hypertableaux, Gleichheit und Anwendungen
  Hypertableaux werden in diesem Vortrag als Spezialform von Tableau- Kalkülen für Prädikatenlogik 1. Stufe diskutiert. Dabei wird auch die Behandlung von Gleichheit vorgestellt und das E-KRHyper-Beweissystem beschrieben. In einem zweiten Teil des Beitrags werden verschiedene Anwendungen skizziert, in denen der KRHyper-Beweiser zum Einsatz kam. Dazu gehören das Living-Book-System und IASON, ein mobiles und personalisiertes Informationssystem. Abschliessend wird ein Vorhaben vorgestellt, wo KRHyper in einem natürlichsprachlichen Antwortsystem als Reasoning-Komponente eingesetzt werden soll.