Home

  Research

  Papers

  Future events

  Event organization

  Invited presentations

  Program committees

  Contact me

  

Current and Past Research Interests

Runtime Verification

My main interest is the development of runtime monitoring techniques, including the design of powerful monitoring logics. See my papers and the following public github repositories: I contributed the parser to this repository and otherwise mentored this work:

Model Checking

I conceptualized and developed during 1998 the first prototype of the Java PathFinder model checker, Java PathFinder 1 (JPF1), a translator from Java to Promela, the modeling language of the SPIN model checker. JPF1 translates a large non-trivial subset of Java 1.0 into Promela, allowing model checking of the Java program.

I was later involved in the initial phase of the development of Java PathFinder 2 (JPF2-...), the second generation of Java PathFinder. The current Java PathFinder project has been run by Willem Visser. JPF2 is written in Java and model checks Java bytecode directly.

I worked for during 1996-1997 at Aalborg University Center with Kim Larsen. Here I studied various protocols from Bang & Olufsen using the UPPAAL real-time model checker. We found a bug that had gone unexplained for 10 years, although its precense was known. The error became important due to a transition from hand-held remote controls to automated control.

Formal Specification Languages

During the years of 1984-1991, I was part of the language design team of the RAISE project. RAISE stands for Rigorous Approach to Industrial Software Engineering, and is a formal software development method, including the very powerful wide-spectrum formal specification language RSL. What is RSL more specifically? There are many ways to present it. Here is one: RSL is a derivation of VDM. Take a standard imperative programming language; add pre-post conditions; predicate logic; notation for manipulating sets, lists and maps; algebraic specification; funtional programming; process algebra; and a module system, and melt it into a unified language. Support it with a framework for refining high level specifications into low-level code. If that sounds too much, then try it, it's in fact not that complicated, and it's a lot of fun. Dines Bjoerner, my first real boss after studies, started this project.

I have unfortunately (by my own fatal choice) been away from this since 1991 when I started my PhD. Here I tried to build an RSL-like language on top of the Concurrent ML (CML) programming language.

See also the book that I co-authored (wrote the majority of): "The RAISE Specification Language", The RAISE Language Group, Prentice-Hall, that is being used at several academic instutions for teaching students about formal methods.

Theorem Proving

I worked during 1994-1996 on theorem proving, trying to prove programs correct using the PVS theorem prover. I wanted to understand what it really means to prove a program correct. I have to say, I believe I got chemically addicted to the Q.E.D. text appearing after each finished PVS proof. Is it possible? I think it is. I had time to do proofs, was sitting in Paris, having expressos, generating Q.E.Ds, and generally feeling pretty good about life. Several visits to SRI, my first entry into the United States. For proof techniques see:

Programming Language Semantics

My master thesis and Ph.D. thesis at DIKU (Datalogisk Institut ved Koebenhavn's Universitet), University of Copenhagen, both contained a large bulk of programming language semantics work. My master thesis was supervised by Neil Jones (the man that made partial evalution work) and resulted in a refinement of an abstract denotational semantics for a small programming language, into a compiler-like denotational semantics, in six steps, each step being more concrete than the former. This work consolidated my interest in functional programming.

My Ph.D. thesis (see my papers) was focused on development of an operational semantics and temporal logic for a process algebra with a fork operator instead of the traditional parallel operator as found in CCS and CSP. It was called the Fork Calculus (FC). Why doing this? .. well my real goal was to develop a temporal logic for Concurrent ML (CML), and CML has a fork operator and not a parallel operator (CML = ML + fork-based concurrency). Believe it or not, but that changes a great deal when it comes to temporal logic for such a language. In order to understand the consequences I had, for practical reasons, to study the problem at a calculus level. An influence was Extended ML (EML= ML + axioms). I attempted to develop an Extended CML (ECML = CML + axioms). My thesis towards the end (after a lot of Fork Calculus theory) contains a proposal for such a language. My supervisors were Klaus Grue (formal supervisor) and Kim Guldstrand Larsen, and I was hosted at Ecole Normale Superieure in Paris with Patrick Cousot, very complicated setup, but it worked (it was impossible to pull me out of Paris). Klaus grue is known for his MAP theory, a unifying framework for computer science and mathematics , combining set theory and the lambda calculus. Kim Larsen is the guy behind the UPPAAL real time model checker, and Patrick Cousot and Radhia Cousot conceptualized abstract interpretation.


Other Services

  • On JPL's board for selection of JPL principles.

  • Serve on JPL's SRS (Senior Research Scientist) Council. A 10 person council (approximately) representing scientists at JPL.

  • Served on the evaluation committee for the INRIA Research Theme: Programs, Verification and Proofs. Report finished May 2015. With Valeria de Paiva, Kathleen Fisher (Chair), Andrew Kennedy, Gerwin Klein, Rustan Leino, Claire Loiseaux, Alan Mycroft, and Luke Ong.

Awards and Recognitions

  • A Workshop (Formal Methods in Outer Space) was organized at ISoLA 2021, Proceedings: Formal Methods in Outer Space, Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday. Whatever the reason was for the organization of this workshop, by Ezio Bartocci, Ylies Falcone, Martin Leucker, I felt very honored. Thanks to the organizers and the contributers.

  • The JPL Magellan award for excellence in research and contribution in the field of runtime verification of software systems. September 2020. Price of 10,000 dollars.

  • Our paper Model checking programs, Willem Visser, Klaus Havelund, Guillaume Brat, and SeungJoon Park, published at ASE 2000, won the 2020 SIGSOFT Impact Paper Award!.

  • Our benchmark paper The DejaVu Runtime Verification Benchmark, K. Havelund, D. Peled, and D. Ulus, won best benchmark price at the RV competition 2018, affiliated with RV 2018, the 18th International Conference on Runtime Verification, 10-13 November 2018 - Limassol, Cyprus.

  • Our paper Monitoring Java Programs with Java PathExplorer, Klaus Havelund and Grigore Rosu, published at The First Workshop on Runtime Verification (RV'01), Paris, France, 23 July 2001. Electronic Notes in Theoretical Computer Science, Volume 55, Number 2, 2001, won the RV 2018 Test of Time award.

  • The JPL Voyager award in recognition of research contributions, including publication record, tool development, and conference organization. August 2017.

  • Our paper Monitoring Programs using Rewriting, Klaus Havelund and Grigore Rosu, published at ASE 2001, has won the ASE 2016 Most Influential Paper award.

  • The LogFire tool (described in this paper) won the offline track (log analysis) of CRV-2015, The 2nd International Competition on Runtime Verification. Held in connection with RV'15, The 15th International Conference on Runtime Verification, September 22 - September 25, 2015 Vienna, Austria.

  • Our paper Model checking programs, Willem Visser, Klaus Havelund, Guillaume Brat, and SeungJoon Park, published at ASE 2000, won the ASE 2014 Most Influential Paper award.

  • The JPL Mariner award in recognition of significant and sustained efforts to establish a new tool-based checking capability for a broad range of coding standards (C, C++, and Java) at JPL. August 2011.

  • Best paper award for: Runtime Verication with State Estimation, S. D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S. A. Smolka, and E. Zadok. Presented at The 2nd International Conference on Runtime Verification (RV 2011) San Francisco, California, USA, October 27-30, 2011.

  • The JPL Ranger award for the development of a Java Coding Standard and its implementation as an automated code checker. July 2010.

  • The JPL Mariner award for the successful delivery of the LogScope tool for MSL (Mars Science Laboratory). LogScope checks output log files against a formal specification and reports violations. The tool was delivered to the FIT [testing] team to support flight software testing. July 2009

  • Outstanding Technology Development Award for Java PathFinder (JPF), Federal Laboratory Consortium (FLC) Far West Region Awards. July 2009.

  • Royal Academy of Engineering Distinguished visiting fellowship, University of Manchester, 2008-2009.

  • ACM Distinguished Paper Award for the paper: Racer: Effective Race Detection Using AspectJ, Eric Bodden and Klaus Havelund. Presented at the International Symposium on Software Testing and Analysis (ISSTA'08), Seattle, WA, July 2008.

  • NASA's Group Achievement Award to the Launch Control System Proof-of-Concept team. For successful demonstration of KSC's Launch Control System Proof-of-Concept Architecture for the Constellation Program's Command, Control and Communication Project. Signed by NASA's Administrator, Michael D. Griffin, Washington DC, "this eighth day of May Two Thousand Eight".

  • Award for contribution to a NASA Tech Brief article for ARC-15244-1, Automated Testing using Symbolic Execution and Temporal Monitoring that highlights a NASA Ames innovation. September 2006.

  • NASA Office of Aerospace Technology Turning Goals Into Reality (TGIR) Engineering Innovation Award for the Java PathFinder (JPF). See story. June 2003.

  • EASST award for best software science paper presented at ETAPS'02: Synthesizing Monitors for Safety Properties, Klaus Havelund and Grigore Rosu. Presented at the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), Grenoble, France, April 2002.

Former Collaborative Projects

Survivable Software

A GCC-based framework for C program instrumentation, program monitoring, and static analysis.

The project developed the InterAspect program-instrumentation framework for GCC.
CMACS Computational Modeling and Analysis for Complex Systems

Also known as "Model Checking and Abstract Interpretation" (MCAI 2.0). NSF Expeditions project.

Teaching

As Appointed Lecturer in Computer Science at California Institute of Technology, 2008 and 2009:


CS119 Part II : Program Monitoring, 2008
Class given at California Institute of Technology, from April 28 - May 29, 2008.



CS119 Part II : Program Monitoring, 2009
Class given at California Institute of Technology, May, 2009.

Free website templates