J-GLOBAL         Last updated: Oct 4, 2011 at 11:29
National Institute of Informatics, Tokyo
DAAD - Research at International Science and Technology Centers
Job title
Visiting Researcher, Host: Prof. Shin Nakajima Ph.D.
Dr. rer. nat.


Recent Projects:

SMTreloaded – SMT-based Model Checking with Relational Logic Added

SMTreloaded aims at supporting sets and relations in software model checking, based on description logics and satisfiability modulo theories (SMT). SMT enables the integration of decision procedures for background theories into a SAT-solving environment. The flexibility, expressiveness, performance of SMT-based methods have attracted the interest of the software verification community. State-of-the-art SMT-solver support first-order theories for arrays, bit vectors, and linear arithmetic. Sets and relations, although being considered as useful for verifying software, are not supported, yet.
We propose description logics as a decidable background theory for sets and relations, the extension of the SMT-solver OpenSMT with decision procedures for description logics, and the integration of the extended SMT-solver into the model checking environment SAL. Both higher expressiveness and better performance for relational structures as compared to existing model checkers are targeted.

CITE - From Counterexamples to Interactive Incremental Tracing of Errors

CITE aims at developing the fundamental methods for generating both comprehensive and comprehensible error reports based on model checking results.
Model checking is a powerful and efficient method for finding flaws in hardware designs, object-oriented software, business processes, and hypermedia applications. One remaining major obstacle to a broader application of model checking is its limited usability for non-experts. It requires much effort and insight to determine the root cause of errors from counterexamples generated by model checkers in the case of a specification violation. The CITE project addresses this problem in two ways: First, a new interactive and incremental process of generating counterexamples is proposed which supports focused successive refinement of verification results at the user’s demand, thus avoiding information overflow caused by bulky counterexamples. Second, a relational representation layer, based on temporal description logics, enables error tracing along semantic relationships of objects. First results indicate that the combination of these methods provides unmatched user support in error tracking while maintaining full compatibility with existing model checking tools and applications.

For further information and publications related to the CITE project, check the Verdikt project at the University of Passau: www.verdikt.uni-passau.de

Research Areas

  • Informatics / Software / Formal Methods and Verification

Academic & Professional Experience

Sep 2009
DAAD Visiting Researcher, National Institute of Informatics, Tokyo:
Jun 2008
Aug 2009
Postdoc Researcher, Chair of Information Management, University of Passau:
Oct 2004
Jun 2008
Research and Teaching Assistant, Chair of Information Management, University of Passau:
May 2001
Sep 2004
Research Assistant, Institute for Information Systems and Software Engineering, University of Passau:
Oct 1996
May 2001
Informatics (Diplom), University of Passau:

Awards & Honors

Nov 2009
Dissertation award for distinctive young researchers of the University of Passau., University of Passau:
Feb 2009
Nomination for the national dissertation award of the German association for computer science (Gesellschaft fuer Informatik), Faculty of Informatics and Mathematics, University of Passau:

Published Papers

see http://www.im.uni-passau.de/db/literatur?who=weitl

Teaching Experience