Skip to main content
These web pages use cascading style sheet features for formatting. You may still browse the text of the site, but for best results, use a modern CSS-enabled browser.

Laboratory for Reliable Software (LaRS)
at the Jet Propulsion Laboratory

Title Image

Klaus Havelund

Klaus's Picture
Jet Propulsion Laboratory
M/S 301-450C
4800 Oak Grove Drive
Pasadena, CA 91109
klaus at havelund dot com


    • MSc Computer Science, University of Copenhagen, Denmark (1986)
    • PhD Computer Science, University of Copenhagen, Denmark (1994)

Professional Experience

    • Senior Research Scientist (2009), Jet Propulsion Laboratory, LaRS
    • Principal Computer Scientist (2007), Jet Propulsion Laboratory, LaRS
    • Researcher (2006), Columbus Technologies / Jet Propulsion Laboratory, LaRS
    • Researcher (1997-2005), NASA Ames Research Center
    • Researcher (1996-1997), Computer Science Dept., Aalborg University, Denmark
    • Researcher (1994-1996), LITP, Paris, France
    • Postdoc (1994), Ecole Polytechnique, Paris, France

Selected Awards

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

Book Chapters

    • The RAISE Language Group. The RAISE Specifcation Language. Prentice Hall, 1992. Chris George,Peter Haff, Klaus Havelund, Anne Haxthausen, Robert Milne, Claus Bendix Nielsen, Soeren Prehn and Kim Ritter Wagner.
    • Klaus Havelund. RAISE in Perspective. Invited chapter in Logics of Specifcation Languages. Edited by Dines Bjorner and Martin Henson. Monographs in Theoretical Computer Science, EATCS Series, 2007, 624p.

Selected Recent Publications

    • Rahul Agarwal, Saddek Bensalem, Eitan Farchi, Klaus Havelund, Yarden Nir-Buchbinder, Scott D. Stoller, Shmuel Ur, and Liqiang Wang. Detection of Deadlock Potentials in Multi-Threaded Programs. September 2010. (Under review).
    • Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Mike Lowry, Corina Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, and Rich Washington. Combining Test-Case Generation and Runtime Verifcation. Journal of Theoretical Computer Science, 336(2-3), May 2005.
    • Cyrille Artho, Klaus Havelund, and Armin Biere. High-Level Data Races. Software Testing, Verifcation and Reliability, 13(4), 2004.
    • Alex Groce, Klaus Havelund, Margaret Smith, and Howard Barringer. Let's Look at the Logs: Low-Impact Runtime Verifcation. July, 2009. (Under review).
    • H. Barringer, D. Rydeheard and K. Havelund. Rule Systems for Run-Time Monitoring: from Eagle to RuleR. Journal of Logic and Computation (To appear).
    • D. Bjorner, A. Haxthausen, and K. Havelund. Formal, Model-oriented Software Development Methods: From VDM to ProCoS and from RAISE to LaCoS. Future Generation Computer Systems, 7, 1992.
    • Eric Bodden and Klaus Havelund. Racer: Effective Race Detection Using AspectJ. IEEE Transactions on Software Engineering. (To appear).
    • + More