Home

  Research

  Papers

  Future Events

  Workshops

  Invited presentations

  Program committees

  Contact me

  

Research

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.


Free website templates