Contact    Jobs
Search:

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

  • Best paper of track B (Logic, Semantics, and Theory of Programming) of ICALP 2009.

Tools

  • dvt: deductive verification of reactive systems and translation validation.
  • MoCS: synthesis of monitor circuits from linear time temporal logic properties.
  • CirView: a small tool for 3D visualization of LTL path checking via boolean circuits.

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.