Lars Kuhtz

photo Lars Kuhtz

Reactive Systems Group
Universität des Saarlandes
Phone: +49 681 302 5477
Fax: +49 681 302 5636
eMail: kuhtz at cs.uni-sb.de

Building: E 1.3 Room: 533

I defended my Ph.D. thesis in December 2010.
Currently, I am employed at Microsoft in Redmond, WA, USA.

Research

During the time as a Ph.D. student, my research was about the complexity of runtime verification of temporal
logic properties. In runtime verification, we monitor the running system and
check on-the-fly whether the desired properties hold. Unlike in static
verification, where the verification algorithm is executed at design-time and
can therefore afford to spend significant time and resources, runtime
verification algorithms must run in synchrony with the monitored system and
usually even share the resources of the implementation platform.

Many questions concerning the complexity of runtime verification problems are
still open. For instance until recently the best known upper bound for the
evaluation of an LTL formula over a (finite) path was P while the best known
lower bound is NC1. We were able to reduce
this gap by proving that path checking for LTL is efficiently
parallelizable.

Runtime verification is often applied within an online monitoring setting where
a possibly infinite input trace is read sequentially. A monitor for online
runtime verification of LTL properties requires in the worst case a number of
states that is doubly exponential in the size of the property. Fortunately, in
practice the worst case often can be avoided. Namely, we provide a construction
of monitor circuits for LTL with bounded and unbounded
future where bounded sub-formulas do not provide to
the exponential blow up.

Formerly, I have been studying random graphs. We developed an algorithm for
approximating the chromatic number of a random graph in expected polynomial
time. Moreover, I built a tool for deductive verification of reactive systems
and translation validation.

Publications

[KF11b] Lars Kuhtz and Bernd Finkbeiner. Weak Kripke Structures and LTL. CONCUR 2011, 2011.
[KF11a] Lars Kuhtz and Bernd Finkbeiner. Efficient Parallel Path Checking for Linear-Time Temporal Logic with Past and Bounds (Preprint). Accepted for publication in Logical Methods in Computer Science, 2011.
[K10] Lars Kuhtz. Model Checking Finite Paths and Trees. Dissertation, Universität des Saarlandes, 2010.
[KF09] Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. ICALP 09, 2009. Best Paper Award.
[FK09] Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with Bounded and Unbounded Future. RV 09, 2009.
[CK06] Amin Coja-Oghlan and Lars Kuhtz. An improved algorithm for approximating the chromatic number of Gn, p. Information Processing Letters 99 (2006), 234-238.
[K04b] Lars Kuhtz. Colouring Gn,p and Spectral Techniques. Diplomarbeit, 2004.
[K04a] Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universität zu Berlin, 2004.

Awards

Tools

Miscelaneous Slides

Recent Student Projects

[M05] Ghulam Mujtaba. Monitoring Execution Traces using Metric Alternating Automata. Master Thesis
[Eme05] Pavel Emeliyanenko. Automatic Verification of Conditions for Absence of Interrupts. Bachelor Thesis
[E07] Franziska Ebert. Translation Validation for Optimizing Compilers. Master Thesis. 2007

Teaching

Projects

My research was supported by the German Research Foundation (DFG) as part of the
Transregional Collaborative Research Center Automatic Verification and
Analysis of Complex Systems (SFB/TR 14 AVACS).

The goal of the AVACS project is to raise the state of the art in automatic
verification and analysis techniques from its current level, where it is
applicable only to isolated facets (concurrency, time, continuous control,
stability, dependability, mobility, data structures, hardware constraints,
modularity, levels of refinement), to a level allowing the comprehensive
verification of computer systems.