Home

  Research

  Papers

  Future events

  Event organization

  Invited presentations

  Program committees

  Contact me

  

Projects
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.
Survivable Software

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

The project has developed the InterAspect 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

Runtime Verification

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 Eagle 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.

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. 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 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. If you want to know more, contact my colleagues from the past Jan Storbank Pedersen (jnp@terma.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 methods. It can be acquired from TERMA.

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.

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.


Awards

  • 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.

Free website templates