Papers Published or Submitted for Publication

• A Case Study in DSL Development - An Experiment with Python and Scala
  K. Havelund, M. Ingham, and D. Wagner
  Scala Days 2010, Arpil 15-16, 2010, Lausanne, Switzerland.
  pdf

• Formal Analysis of Log Files
  H. Barringer, A. Groce, K. Havelund and M. Smith
  Journal of Aerospace Computing, Information, and Communication, February 2010.
  Invited talk given at the SMC-IT workshop: Software Reliability for Space Missions. July 20, 2009, Pasadena, California, USA.
  pdf (to appear, currently being reformatted to single space format by editor)

• Prototyping a Domain-Specific Language for Monitor and Control Systems
  M. Bennett, R. Borgen, K. Havelund, M. Ingham and David Wagner
  Journal of Aerospace Computing, Information, and Communication, January 2010.
  Extended version (extended with a study of the Scala programming language for DSL development) of paper submitted to IEEE Aerospace Conference Big Sky, Montana, March 1-8, 2008 (see below).
  pdf (to appear, currently being reformatted to single space format by editor)

• From Scripts to Specifications
  A. Groce, K. Havelund, and M. Smith
  ACM/IEEE 32nd International Conference on Software Engineering (ICSE 2010)
  Cape Town, South Africa, May 2-8, 2010.
  The work received JPL's internal Mariner Award in August 2009.
  pdf

• Detection of Deadlock Potentials in Multi-Threaded Programs
  R. Agarwal , S. Bensalem , E. Farchi , K. Havelund , Y. Nir-Buchbinder, S. D. Stoller, S. Ur, and L. Wang
  IBM Journal of Research & Development, 2010
  To appear.

• Rule Systems for Runtime Verification: A Short Tutorial
  H. Barringer, K. Havelund, D. Rydeheard, A. Groce
  Tutorial presented at the 9th international workshop on Runtime Verification (RV'09).
  Lecture Notes in Computer Science volume 5779.
  Grenoble, France, June 26-28, 2009.
  pdf

• An Entry Point for Formal Methods: Specification and Analysis of Event Logs
  H. Barringer, A. Groce, K. Havelund, M. Smith
  Invited talk given at the 1'st Workshop on Formal Methods in Aerospace (FMA'09).
  Affiliated with FM'09.
  To appear in Electronic Proceedings of Theoretical Computer Science (EPTCS).
  Eindhoven, Holland, November 3, 2009.
  pdf (abstract published in informal hand-out proceedings: pdf)

• Establishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, and Monitoring
  A. Groce, K. Havelund, G. Holzmann, R. Joshi, R-G. Xu
  Submitted to Annals of Mathematics and Artificial Intelligence.
  Under review.

• Requirements Capture with RCAT
  M. Smith and K. Havelund
  16th IEEE International Requirements Engineering Conference
  Barcelona, Spain, September 8-12, 2008.
  pdf

• Racer: Effective Race Detection Using AspectJ
  E. Bodden and K. Havelund
  IEEE Transactions of Software Engineering (invited journal version of ISSTA'08 paper, to appear)
  pdf

• Racer: Effective Race Detection Using AspectJ
  E. Bodden and K. Havelund
  International Symposium on Software Testing and Analysis (ISSTA'08)
  Seattle, WA, July 20-24, 2008.
  Won ISSTA's ACM SIGSOFT Distinguished Paper Award.
  pdf
  (here is the technical report)

• Automated Testing of Planning Models
  Klaus Havelund, Alex Groce, Gerard Holzmann, Rajeev Joshi, and Margaret Smith
  The Fifth International Workshop on Model Checking and Artificial Intelligence (MOCHART'08 @ ECAI'08)
  Lecture Notes in Artificial Intelligence (LNAI), Volume 5348.
  Patras, Greece, July 21, 2008.
  pdf

• Runtime Verification of C Programs
  K. Havelund
  TestCom/FATES conference
  Lecture Notes in Computer Science volume 5047.
  Tokyo, Japan, June 10-13, 2008.
  pdf

• Aspect-Oriented Monitoring of C Programs
  K. Havelund and E. V. Wyk
  The Sixth IARP-IEEE/RAS-EURON Joint Workshop on Technical Challenges for Dependable Robots in Human Environments
  Pasadena, CA, May 17-18, 2008.
  pdf

• Development of a Prototype Domain-Specific Language
  for Monitor and Control Systems
  M. Bennett, R. Borgen, K. Havelund, M. Ingham and David Wagner
  IEEE Aerospace Conference (URL)
  Big Sky, Montana, March 1-8, 2008.
  pdf

• Visualization of Concurrent Program Executions
  C. Artho, K. Havelund and S. Honiden
  Workshop on Software Architectures and Component Technologies (SACT'07 @ COMPSAC'07)
  Beijing, China, July 23, 2007.
  pdf

• Rule Systems for Run-Time Monitoring: from Eagle to RuleR
  H. Barringer, D. Rydeheard and K. Havelund
  Journal of Logic and Computation (JLC).
  Journal version of RV'07 paper
  pdf

• Rule Systems for Run-Time Monitoring: from Eagle to RuleR
  H. Barringer, D. Rydeheard and K. Havelund
  7th International Workshop on Runtime Verification (RV'07 @ AOSD'07)
  Vancouver, Canada, March 13, 2007.
  pdf (extended abstract)
  pdf (full version).
  Lecture Notes in Computer Science volume 4839.

• Towards the Industrial Scale Development of Custom Static Analyzers
  J. Anton, E. Bush, A. Goldberg, K. Havelund, D. Smith and A. Venet
  Static Analysis Summit (webpage)
  U.S. National Institute of Standards and Technology
  Gaithersburg, MD, USA, June 29, 2006.
  pdf

• Confirmation of Deadlock Potentials Detected by Runtime Analysis
  S. Bensalem, J.-C. Fernandez, K. Havelund and L. Mounier
  Parallel and Distributed Systems: Testing and Debugging 2006 (PADTAD'06)
  Seattle, Maine, USA, July 17, 2006.
  Invited paper/talk.
  pdf

• Dynamic Deadlock Analysis of Multi-Threaded Programs
  S. Bensalem and K. Havelund
  Parallel and Distributed Systems: Testing and Debugging 2005 (PADTAD'05)
  Haifa, Israel, November 15, 2005.
  Lecture Notes in Computer Science volume 3875.
  pdf, slides
  

• Verify Your Runs
  K. Havelund and A. Goldberg
  Verified Software: Theories, Tools, Experiments (VSTTE'05)
  Zurich, Switzerland, October 10-13, 2005
  pdf

• Automated Runtime Verification with Eagle
  A. Goldberg and K. Havelund
  Workshop on Verification and Validation of Enterprise Information Systems (VVEIS'05)
  Miami, Florida, USA, May 24, 2005
  pdf
  

• Event-Based Runtime Verification of Java Programs
  Combining Runtime Verification with Aspect Oriented Programming
  M. d'Amorim and K. Havelund
  Workshop on Dynamic Analysis (WODA'05)
  St. Louis, Missouri, USA, May 17, 2005
  pdf
  

• Runtime Verification for Autonomous Space Craft Software
  A. Goldberg, K. Havelund and C. McGann
  IEEE Aerospace Conference
  Big Sky, Montana, USA, March 5-12, 2005
  word
  

• Toward a Framework and Benchmark for Testing Tools for Multi-Threaded Programs
  Y. Eytani, K. Havelund, S. Stoller and S. Ur
  To appear in the journal Concurrency and Computation: Practice and Experience, Wiley. 2005.
  pdf
  

• Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors
  C. Artho, K. Havelund, and A. Biere
  2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04),
  Taiwan, October 31-November 3, 2004.
  pdf
  

• Program Monitoring with LTL in Eagle
  H. Barringer, A. Goldberg, K. Havelund and K. Sen
  PADTAD'04, Parallel and Distributed Systems: Testing and Debugging
  Santa Fe, New Mexico, USA, April 30, 2004
  pdf

• Rule-Based Runtime Verification
  H. Barringer, A. Goldberg, K. Havelund and K. Sen
  VMCAI'04, Fifth International Conference on Verification, Model Checking and Abstract Interpretation, January 11-13, Venice, Italy, 2004.
  pdf
  

• Applying Jlint to Space Exploration Software
  C. Artho and K. Havelund
  VMCAI'04, Fifth International Conference on Verification, Model Checking and Abstract Interpretation, January 11-13, Venice, Italy, 2004.
  pdf
  

• High-Level Data Races
  C. Artho, K. Havelund and A. Biere
  Journal of Software Testing, Verification and Reliability (STVR), 13(4).
  Extended version of VVEIS'03 paper.
  pdf
  

• High-Level Data Races
  C. Artho, K. Havelund, and A. Biere
  VVEIS'03, The First International Workshop on Verification and Validation of Enterprise Information Systems
  Angers, France, April 22, 2003.
  pdf
  

• Instrumentation of Java Bytecode for Runtime Analysis
  A. Goldberg and K. Havelund
  FTfJP'03, Fifth ECOOP Workshop on Formal Techniques for Java-like Programs, Darmstadt, Germany, July 21, 2003.
  pdf
  

• Execution-Based Model Checking of Interrupt-Based Systems
  D. Drusinsky and K. Havelund
  Workshop on Model Checking for Dependable Software-Intensive Systems. Affiliated with DSN'03, The International Conference on Dependable Systems and Networks. San Francisco, CA, USA, June 22-25, 2003.
  pdf
  

• Experimental Evaluation of Verification and Validation Tools on Martian Rover Software
  G. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, W. Visser, R. Washington
  Formal Methods in System Design, 25(2), 2004
  Journal version of CMU/SEI paper with same name.
  pdf
  

• Experimental Evaluation of Verification and Validation Tools on Martian Rover Software
  G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser.
  CMU/SEI Software Model Checking Workshop, Pittsburg, USA, March 24, 2003.
  pdf
  

• Benchmark and Framework for Encouraging Research on Multi-Threaded Testing Tools
  K. Havelund, S. Stoller, and S. Ur
  Invited paper (Shmuel Ur is the invited speaker).
  PADTAD'03, Parallel and Distributed Systems: Testing and Debugging
  Nice, France, April 22-26, 2003
  pdf

• Combining Test-Case Generation and Runtime Verification
  C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser and R. Washington
  Journal of Theoretical Computer Science, Vol. 336 Number 2-3.
  Special issue: "Abstract State Machines and High-Level System Design and Analysis", May 2005.
  Extended version of ASM'03 paper: "Experiments with Test Case Generation and Runtime Analysis".
  pdf

• Experiments with Test Case Generation and Runtime Analysis
  C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu and W. Visser
  I am invited speaker.
  ASM 2003, 10th International Workshop on Abstract State Machines
  Taormina, Italy, March 3-7, 2003
  pdf

• Program Instrumentation and Trace Analysis
  K. Havelund, A. Goldberg, R. Filman, G. Rosu
  Invited paper.
  Monterey Workshop 2002
  Radical Innovations of Software and Systems Engineering in the Future
  Venice, Italy, October 7-11, 2002
  Abstract rtf (word)

• Program Model Checking as a New Trend
  K. Havelund, W. Visser
  Guest editorial arcticle in special issue on SPIN'00 that was organized by the authors.
  International Journal on Software Tools for Technology Transfer (STTT) 4(1), 2002. Special STTT journal issue containing selected submissions for the 7'th SPIN workshop, Stanford, August 30-31, September 1 2000, organized by the authors
  pdf

• The Effect of AOP on Softare Engineering, with Particular Attention to OIF and Event Quantification
  R. Filman and K. Havelund
  Workshop on Software Engineering Properties of Languages for Aspect Technologies (SPLAT '03), Boston, USA, 2003.
  pdf
  

• Realizing Aspects by Transforming for Events
  R. E. Filman and K. Havelund
  Automated Software Engineering 2002 (ASE'02), Edinburgh, Scottland, 23-27 September 2002, IEEE Computer Society
  pdf

• Efficient Monitoring of Safety Properties
  K. Havelund and G. Rosu
  To appear in the journal Software Tools for Technology Transfer, 2004.
  Extended version of the paper "Synthesizing Monitors for Safety Properties" that was presented at TACAS'02.
  pdf
  

• Synthesizing Monitors for Safety Properties
  K. Havelund and G. Rosu
  International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02),
  Grenoble, France, 6-14 April 2002
  Won EASST award for best software science paper presented at ETAPS'02
  ps, ps.gz

• Source-Code Instrumentation and Quantification of Events
  R. E. Filman and K. Havelund
  Foundations of Aspect-Oriented Languages (FOAL'02), Enschede, The Netherlands, April 22, 2002.
  pdf

• Rewriting-Based Techniques for Runtime Verification
  G. Rosu and K. Havelund
  To appear in the journal of Automated Software Engineering, 2004.
  Substantially expanded version of "Monitoring Programs using Rewriting" that was presented at ASE'01.
  pdf
  

• Monitoring Programs using Rewriting
  K. Havelund and G. Rosu
  Automated Software Engineering 2001 (ASE'01), San Diego, California, 26-29 November 2001, IEEE Computer Society
  ps, ps.gz

• Automata-Based Verification of Temporal Properties on Running Programs
  D. Giannakopoulou and K. Havelund
  Automated Software Engineering 2001 (ASE'01), San Diego, California, 26-29 November 2001, IEEE Computer Society
  pdf, pdf.gz (Extension of paper as a RIACS Technical Report TR 01-21, August 2001)

• Specification and Error Pattern Based Program Monitoring
  K. Havelund, Scott Johnson and G. Rosu
  European Space Agency Workshop on On-Board Autonomy, Noordwijk, Holland, 17-19 October 2001
  ps, ps.gz

• An Overview of the Runtime Verification Tool Java PathExplorer
  K. Havelund and G. Rosu
  Formal Methods in System Design, 24(2), March 2004.
  Extended version of the paper "Monitoring Java Programs with Java PathExplorer" presented at RV'01.
  pdf
  

• Monitoring Java Programs with Java PathExplorer
  K. Havelund and G. Rosu
  First Workshop on Runtime Verification (RV'01), Paris, France, 23 July 2001. Electronic Notes in Theoretical Computer Science, Volume 55, Number 2, 2001
  ps, ps.gz

• Java PathExplorer - A Runtime Verification Tool
  K. Havelund and G. Rosu
  The 6th International Symposium on AI, Robotics and Automation in Space, May 2001
  ps, ps.Z

• Using Runtime Analysis to Guide Model Checking of Java Programs
  K. Havelund
  The 7th International SPIN Workshop, Stanford, California, August-September, 2000
  ps, ps.Z

• Model Checking Programs
  W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda
  International Journal on Automated Software Engineering 10(2), April 2003.
  Extended journal version of paper presented at the ASE'00 conference
  pdf

• Model Checking Programs
  W. Visser, K. Havelund, G. Brat, S. Park
  International Conference on Automated Software Engineering. September 2000
  ps, ps.Z

• Java PathFinder - Second Generation of a Java Model Checker
  W. Visser, K. Havelund, G. Brat, S. Park
  Post-CAV Workshop on Advances in Verification July 2000
  ps, ps.Z

• Mapping Temporal Planning Constraints into Timed Automata
  L. Khatib, N. Muscettola, K. Havelund
  Time'01 (IEEE press), The Eighth International Symposium on Temporal Representation and Reasoning, Cividale Del Friuli, Italy, 2001.
  pdf
  

• Verification of Plan Models Using UPPAAL
  L. Khatib, N. Muscettola, K. Havelund
  First International Workshop on Formal Approaches to Agent-Based Systems, NASA's Goddard Space center, LNCS/LNAI-1871, Maryland, March 2000
  pdf

• Formal Analysis of the Remote Agent - Before and After Flight
  K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, Jon L. White
  The Fifth NASA Langley Formal Methods Workshop, Virginia, June, 2000
  ps, ps.Z

• Adding Active Objects to SPIN
  W. Visser, K. Havelund, J. Penix
  Appeared in proceedings of 5th SPIN Workshop, July 1999, Trento
  ps, ps.Z

• Applying Model Checking in Java Verification
  K. Havelund, J. Skakkebaek
  Proceedings of 6th SPIN Workshop in connection with FM99 Toulouse
  ps, ps.Z

• Model Checking Java Programs Using Java PathFinder
  K. Havelund, T. Pressburger
  International Journal on Software Tools for Technology Transfer (STTT) 2(4), April 2000. Special issue containing selected submissions for the 4'th SPIN workshop, Paris, November 1998
  ps, ps.Z

• Java PathFinder, A Translator from Java to Promela
  K. Havelund
  Theoretical and Practical Aspects of SPIN Model Checking, Toulouse, France, September, 1999
  pdf
  

• Formal Analysis of a Space Craft Controller using SPIN
  K. Havelund, M. Lowry, J. Penix
  IEEE Transactions on Software Engineering, Volume 27, Number 8, August 2001. Originally appeared in proceedings of the 4th SPIN Workshop, November 1999, Paris
  ps, ps.gz
  ps, ps.Z (Extended Technical Report)

• Mechanical Verification of a Garbage Collector
  K. Havelund
  FMPPTA'99
  ps, ps.Z
  ps, ps.Z (Tech. report)

• Transformation Systems at NASA Ames
  W. Buntine, B. Fischer, K. Havelund, M. Lowry, T. Pressburger, S. Roach, P. Robinson, J. V. Baalen
  STS'99
  ps, ps.Z

• Formal Verification of an Audio/Video Power Controller using the Real-Time Model Checker UPPAAL
  K. Havelund, K.G. Larsen, A. Skou
  ARTS'99
  ps, ps.Z
  ps, ps.Z] (Tech. report)

• Using Model Checking to Validate AI Planner Domain Models
  J. Penix, C. Pecheur, K. Havelund
  SEL'98
  ps, ps.Z

• Verification and Validation of AI Systems that Control Deep-Space Spacecrafts
  M. Lowry, K. Havelund, J. Penix
  ISMIS'97
  ps, ps.Z

• Declarative Specification of Software Architectures
  J. Penix, P. Alexander, K. Havelund
  ASE'97
  ps, ps.Z

• Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL
  K. Havelund, A. Skou, K.G. Larsen, K. Lund
  RTSS'97
  ps, ps.Z

• Experiments in Theorem Proving and Model Checking
  K. Havelund, N. Shankar
  FME'96
  ps, ps.Z
  ps, ps.Z (Tech. report)

• The Fork Calculus
  K. Havelund, K.G. Larsen
  ICALP'93, and Nordic Journal of Computing 94
  dvi, dvi.Z
  dvi, dvi.Z (Long version with proofs)

• A Refinement Logic for the Fork Calculus
  K. Havelund, K.G. Larsen
  PSTV'94
  ps, ps.Z

• Formal, Model-oriented Software Development Methods: From VDM to ProCoS and from RAISE to LaCoS
  D. Bjorner, A. Haxthausen and K.Havelund
  Future Generation Computer Systems, volume 7, North-Holland, 1992.
  acm portal

• The RAISE Language, Method and Tools
  C. George, K. Havelund, M. Nielsen, and K. R. Wagner
  Formal Aspects of Computing 1(1), Springer International, 1989
  Journal version of LNCS 328 paper of same name.
  SpringerLink

• The RAISE Language, Method and Tools
  M. Nielsen, K. Havelund, K. R. Wagner and C. George
  In: VDM - The Way Ahead, LNCS 328, 1988.
  Electronic copy not available.

Books and Book Chapters

• RAISE in Perspective
  Klaus Havelund
  Chapter in Logics of Specification Languages
  Monographs in Theoretical Computer Science. An EATCS Series, 2007
  Bjorner, Dines; Henson, Martin C. (Eds.)
  624 p., Hardcover
  
  The brief chapter (4 pages) comments on RSL, the RAISE Specification Language.

• The RAISE Specification Language
  The RAISE Language Group
  Prentice Hall. The BCS Practitioner Series, 1992.
  For sale at amazon.com
  
  The book consists of two parts I: RSL Tutorial (pages 9-250), and II: RSL Reference Description (pages 251-369).
  Havelund wrote part I, while Havelund together with Anne Haxthausen wrote part II. The language presented in the book was designed during the period 1985-1991 by many people. Those that lastet to the end were the RAISE Language Group: Chris George, Peter Haff, Klaus Havelund, Anne Haxthausen, Robert Milne, Claus Bendix Nielsen, Soeren Prehn and Kim Ritter Wagner. The RAISE project was started by Dines Bjoerner.

Theses

• The Fork Calculus - Towards a Logic for Concurrent ML
  K. Havelund
  Ph.D. thesis
  DIKU, Department of Computer Science, University of Copenhagen, Denmark, 1994.
  Supervisors: Klaus Grue and Kim Guldstrand Larsen.
  Performed at Ecole Normale Superieure, Paris, France, while attending the groups of Michel Bidoit and Patrick Cousot.
  ps

• Stepwise Development of a Denotational Stack Semantics
  K. Havelund
  Master thesis
  DIKU, Department of Computer Science, University of Copenhagen, Denmark, 1984.
  Supervisor: Neil Jones.
  Electronic copy is not available (lost in one of many computer-to-computer moves).
  If you have a copy, let me know.

Some Technical Reports

• Eagle Monitors by Collecting Facts and Generating Obligations
  H. Barringer, A. Goldberg, K. Havelund, and K. Sen
  Technical Report: Pre-Print CSPP-25, University of Manchester, Department of Computer Science, October 2003.
  pdf
  

• Eagle Does Space Efficient LTL Monitoring
  H. Barringer, A. Goldberg, K. Havelund, and K. Sen
  Technical Report: Pre-Print CSPP-25, University of Manchester, Department of Computer Science, October 2003
  pdf
  

• Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae
  G. Rosu and K. Havelund
  RIACS Technical Report TR 01-15, May 2001. Written 15 January 2001
  ps, ps.gz

• Testing Linear Temporal Logic Formulae on Finite Execution Traces
  K. Havelund and G. Rosu
  RIACS Technical Report TR 01-08, May 2001. Written 20 December 2000
  ps, ps.gz

• Java PathFinder User Guide
  K. Havelund
  Unpublished Report
  ps, ps.Z

• Java PathFinder, A Translator from Java to Promela
  K. Havelund and T. Pressburger
  Unpublished Report, 1998
  pdf

• A Mechanized Refinement Proof for a Garbage Collector
  K. Havelund, N. Shankar
  (Unsubmitted)
  ps, ps.Z
  ps, ps.Z (Unpublished report)

• StateText - A Textual Language for State Charts with Data
  K. Havelund, K. G. Larsen
  (Unpublished report)
  ps, ps.Z