Logics for Program Analysis
In search for a satisfactory runtime verification logic: convenient to use, expressive, covering state machines a
well as logic, efficient to monitor,
and easy to implement.
A GCC-based framework for C program instrumentation, program monitoring, and static analysis.
The project has developed the
program-instrumentation framework for GCC.
Computational Modeling and Analysis for Complex Systems
Also known as "Model Checking and Abstract Interpretation" (MCAI 2.0).
NSF Expeditions project. My focus will here be inferring specifications from execution traces.
Java Coding Standard
Development of a JPL institutional coding standard for Java. A set of coding rules that
Java programmers should follow.
Current and Past Research Interests
My main interest is the development of runtime monitoring techniques,
including the design of powerful monitoring logics, and algorithms for detecting
concurrency errors such as deadlocks and various forms of data races.
The most recent work includes the RMOR monitoring tool for monitoring C programs against state machines
using aspect oriented techniques.
Previous work includes the very powerful
temporal monitoring logic, implemented in the Eagle Flier trace checker. Eagle supports
user definable logics and combinators, using recursive fixpoint rules and parameterization with
formulas as well as with data. Real-time logics can be defined in few lines of Eagle.
I conceptualized and developed during 1998 the first prototype of
the Java PathFinder model checker,
Java PathFinder 1
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. There are two websites for this project (at least):
RAISE in Denmark and
RAISE in Macau.
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. It even has
tools developed by UNU/IIST.
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
add pre-post conditions;
notation for manipulating sets, lists and maps;
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.
If you want to know more, contact my colleagues
from the past
Jan Storbank Pedersen (email@example.com),
Chris George, or the ultimate source
Dines Bjoerner, my first real boss after studies,
that started all this.
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
It can be acquired from
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.
Programming Language Semantics
My master thesis and Ph.D. thesis at
(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.
- On JPL's board for selection of JPL principles.
- Served 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),
Alan Mycroft, and
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
won the offline track (log analysis) of
The 2nd International Competition on Runtime Verification.
Held in connection with
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.
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.
Outstanding Technology Development Award for Java PathFinder (JPF), Federal Laboratory Consortium
Far West Region Awards.
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
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).
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.
Free website templates