Home

  Research

  Papers

  Future events

  Event organization

  Invited presentations

  Program committees

  Contact me

 

According to the Web

Papers Published or Submitted for Publication

  • nfer - A Notation and System for Inferring Event Stream Abstractions
    S. Kauffman, K. Havelund, and R. Joshi

    RV 2016
    In Ylies Falone and Cesar Sanchez editors, 16th International Conference on Runtime Verification.
    23-30 September 2016 - Madrid. LNCS, Volume 10012, pages 235-250, Springer-Verlag.
    pdf

  • Towards a Unified View of Modeling and Programming
    M. Broy, K. Havelund, and R. Kumar

    ISoLA 2016
    In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Part II. Track: Towards a Unified View of Modeling and Programming, organized by Manfred Broy, Klaus Havelund, Rahul Kumar, and Bernhard Steffen. 10-14 October 2016 - Imperial, Corfu, Greece. LNCS 9952, pages 238-260, Springer-Verlag.
    pdf

  • Towards a Logic for Inferring Properties of Event Streams
    S. Kauffman, R. Joshi, and K. Havelund.

    ISoLA 2016
    In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Part II. Track: RVE - Runtime Verification and Enforcement, the (Industrial) Application Perspective, organized by Ezio Bartocci and Ylies Falcone. 10-14 October 2016 - Imperial, Corfu, Greece. LNCS 9952, pages 333-338, Springer-Verlag.
    pdf

  • What is a Trace? A Runtime Verification Perspective
    G. Reger and K. Havelund.

    ISoLA 2016
    In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Part II. Track: RVE - Runtime Verification and Enforcement, the (Industrial) Application Perspective, organized by Ezio Bartocci and Ylies Falcone. 10-14 October 2016 - Imperial, Corfu, Greece. LNCS 9952, pages 339-355, Springer-Verlag.
    pdf

  • Towards a Unified View of Modeling and Programming (Track Summary)
    M. Broy, K. Havelund, R. Kumar, and B. Steffen.

    ISoLA 2016
    In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Part II. Track: Towards a Unified View of Modeling and Programming, organized by Manfred Broy, Klaus Havelund, Rahul Kumar, and Bernhard Steffen. 10-14 October 2016 - Imperial, Corfu, Greece. LNCS 9952, pages 3-10, Springer-Verlag.
    pdf

  • Static and Runtime Verification, Competitors or Friends? (Track Summary)
    Dilian Gurov, Klaus Havelund, Marieke Huisman, and Rosemary Monahan

    ISoLA 2016
    In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Part I. Track: Static and Runtime Verification, Competitors or Friends?, organized by Dilian Gurov, Klaus Havelund, Marieke Huisman, and Rosemary Monahan. 10-14 October 2016 - Imperial, Corfu, Greece. LNCS 9952, pages 397-401, Springer-Verlag.
    pdf

  • K: A Wide Spectrum Language for Modeling, Programming, and Analysis
    K. Havelund, R. Kumar, C. Delp and B. Clement

    MODELSWARD 2016
    4th International Conference on Model-Driven Engineering and Software Development.
    19-21 February 2016 - Rome, Italy. SCITEPRESS. To appear.
    On short list of candidate papers to win the MODELSWARD 2016 best paper award.
    pdf

  • Verified Change
    K. Havelund and R. Kumar
    To appear in FoMaC: Transactions on Foundations for Mastering Change (edited by Bernhard Steffen). First issue containing submissions from the editorial board. Submitted in final form 2016.
    pdf

  • Some Recent Advances in Automated Analysis
    E. Abraham and K. Havelund
    International Journal on Software Tools for Technology Transfer (STTT), volume 18, issue 2, pages 121-128, 2016. Introduction article to special issue containing selected submissions from TACAS 2014.
    Springer Link
    pdf

  • Domain-Specific Languages with Scala
    C. Artho, K. Havelund, R. Kumar, and Y. Yamagata

    ICFEM 2015
    In Michael Butler, Sylvain Conchon, and Fatiha Zaidi editors, 17th International Conference on Formal Engineering Methods.
    3-6 November 2015 - Paris. LNCS, Volume 9407, pages 1-16, Springer-Verlag.
    pdf

  • Specification of Parametric Monitors - Quantified Event Automata versus Rule Systems
    K. Havelund and G. Reger

    SyDe Summer School 2015
    In Rolf Drechsler and Ulrich Kuhne, editors, Formal Modeling and Verification of Cyber-Physical Systems (book), pages 151-189. 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015.
    pdf

  • Rule-based Runtime Verification Revisited
    K. Havelund
    International Journal on Software Tools for Technology Transfer (STTT), volume 17, issue 2, page 143-170. doi:10.1007/s10009-014-0309-2. Special issue containing selected submissions from the 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2012). Track: Runtime Verification, the Application Perspective. Published online April 2013. Paper version March 2015.
    pdf

  • Experience with Rule-Based Analysis of Spacecraft Logs
    K. Havelund and R. Joshi

    FTSCS 2014
    In Cyrille Artho and Peter Olveczky, editors, FTSCS 2014: Third International Workshop on Formal Techniques for Safety-Critical Systems. 6-7 November 2014 - Luxembourg. Communications in Computer and Information Science (CCIS). Volume 476, pages 1-16, Springer-Verlag. An ICFEM 2014 Satellite Event.
    pdf

  • Comprehension of Spacecraft Telemetry using Hierarchical Specifications of Behavior
    K. Havelund and R. Joshi

    ICFEM 2014
    In Stephan Merz and Jun Pang, editors, 16th International Conference on Formal Engineering Methods.
    3-7 November 2014 - Luxembourg. LNCS, Volume 8829, pages 187-202, Springer-Verlag.
    pdf

  • Data Automata in Scala
    K. Havelund

    TASE 2014
    In Martin Leucker and Ji Wang, editors, The 8th International Symposium on Theoretical Aspects of Software Engineering.
    1-3 September 2014 - Changsha, China. IEEE Computer Society Press. Pages 1-9.
    Invited presentation.
    pdf

  • Monitoring with Data Automata
    K. Havelund

    ISoLA 2014
    In Tiziana Margaria and Bernhard Steffen, editors, 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Statistical Model Checking, Past Present and Future, organized by Kim Larsen and Axel Legay.
    8-11 October 2014 - Imperial, Corfu, Greece. LNCS 8803, pages 254-273, Springer-Verlag.
    pdf

  • Mastering Change @ Runtime
    K. Havelund

    ISoLA 2014
    In Tiziana Margaria and Bernhard Steffen, editors, 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Response to a call for opinion statements from members of the editorial board of the upcoming journal: LNCS Transactions on Foundations for Mastering Change (FoMaC).
    8-11 October 2014 - Imperial, Corfu, Greece. LNCS 8802, pages 533-534, Springer-Verlag.
    pdf

  • 40 Years of Formal Methods - Some Obstacles and Some Possibilities ?
    D. Bjoerner and K. Havelund

    FM 2014.
    Lecture Notes in Computer Science, Vol. 8442.
    D. Bjoerner invited speaker.
    pdf

  • Verification & Validation Meets Planning & Scheduling
    S. Bensalem, K. Havelund, and A. Orlandini
    International Journal on Software Tools for Technology Transfer (STTT) 16(1) 2014. Introduction article to special issue containing selected submissions for the 3rd ICAPS workshop on Verification & Validation of Planning & Scheduling Systems (VVPS 2011).
    pdf

    Also presented at MOCHAP 2014, Workshop on Model Checking and Automated Planning, Portsmouth, NH, USA, June 21-26, 2014. Affiliated with ICAPS 2014, the 24th International Conference on Automated Planning and Scheduling.

  • A Scala DSL for Rete-based Runtime Verification
    K. Havelund

    The 4th International Conference on Runtime Verification (RV 2013)
    Rennes, France, September 24-27, 2013.
    Lecture Notes in Computer Science, Vol. 8174.
    pdf

  • InterAspect: Aspect-Oriented Instrumentation with GCC
    J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund, S. A. Smolka, S. D. Stoller, and E. Zadok

    Formal Methods in System Design, 41(3), 295-320, December 2012.
    Extended version of the paper "Aspect-Oriented Instrumentation with GCC" presented at RV'10.
    pdf

  • Requirements-Driven Log Analysis - Extended Abstract
    K. Havelund

    ICTSS 2012
    In B. Nielsen and C. Weise, editors, 24th IFIP WG 6.1 Int. Conference on Testing Software and Systems.
    19-21 November 2012 - Aalborg, Denmark. LNCS 7641, Springer-Verlag. Invited presentation.
    pdf

  • What does AI have to do with RV? - Extended Abstract
    K. Havelund

    ISoLA 2012
    In T. Margaria and B. Steffen, editors, 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Runtime Verification - the Application Perspective.
    15-18 October 2012 - Heraclion, Crete. LNCS 7610, Springer-Verlag. Invited presentation.
    pdf

  • A Tutorial on Runtime Verification
    Y. Falcone, K. Havelund, and G. Reger

    Book chapter for: Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. July 31 to August 12, 2012. Editors: Manfred Broy, Doron Peled, and Georg Kalus. IOS Press book, 2013. NATO Science for Peace and Security Series - D: Information and Communication Security. Volume 34.
    pdf

  • Introduction to the Special Section on Runtime Verification
    O. Sokolsky, K. Havelund, and Insup Lee
    International Journal on Software Tools for Technology Transfer (STTT) 14(3), 2012. Introduction article to special issue containing selected submissions on runtime verification.
    pdf

  • Quantified Event Automata - Towards Expressive and Efficient Runtime Monitors
    H. Barringer, Y. Falcone, K. Havelund, G. Reger, and D. Rydeheard

    FM 2012.
    Lecture Notes in Computer Science, Vol. 7436.
    pdf

  • Howard Barringer - The Man who Invented the Past
    K. Havelund

    HOWARD-60
    Higher-Order Workshop on Automated Runtime Verification and Debugging.
    December 20, 2011, Manchester, UK.
    EasyChair Proceedings Volume 1 (first edition).
    Festschrift celebrating Howard Barringer's 60th Birthday and hosted by CICADA and CS, the University of Manchester.
    Editors: Andrei Voronkov and Margarita Korovina.
    pdf
    See also online proceedings

  • Closing the Gap Between Specification and Programming: VDM++ and Scala
    K. Havelund

    HOWARD-60
    Higher-Order Workshop on Automated Runtime Verification and Debugging.
    December 20, 2011, Manchester, UK.
    EasyChair Proceedings Volume 1 (first edition).
    Festschrift celebrating Howard Barringer's 60th Birthday and hosted by CICADA and CS, the University of Manchester.
    Editors: Andrei Voronkov and Margarita Korovina.
    Invited presentation.
    pdf
    Where Specification and Programming Meet - Extended Abstract (early version):
    pdf
    See also online proceedings

  • Implementing Runtime Monitors
    K. Havelund

    TORRENTS 2011
    2nd TORRENTS Workshop
    December 12, 2011, Toulouse, France.
    Invited presentation
    pdf

  • Software Certification: Coding, Code, and Coders
    K. Havelund and G. Holzmann

    EMSOFT 2011
    International Conference on Embedded Software
    October 9-14, 2011, Taipei, Taiwan
    Invited presentation
    pdf

  • Runtime Verication with State Estimation
    S. D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S. A. Smolka, and E. Zadok

    The 2nd International Conference on Runtime Verification (RV 2011)
    San Francisco, California, USA, September 27-30, 2011.
    Lecture Notes in Computer Science, Vol. 7186.
    Won best paper award
    pdf

  • Internal versus External DSLs for Trace Analysis
    Extended abstract for presented tutorial.
    H. Barringer and K. Havelund

    The 2nd International Conference on Runtime Verification (RV 2011)
    San Francisco, California, USA, October 27-30, 2011.
    Lecture Notes in Computer Science, Vol. TBD.
    pdf

  • Checking Flight Rules with TraceContract: Application of a Scala DSL for Trace Analysis
    H. Barringer, K. Havelund, E. Kurklu, and R. Morris

    Scala Days 2011 (informal web-based proceedings).
    June 2-3, 2011.
    pdf

  • TraceContract: A Scala DSL for Trace Analysis
    H. Barringer and K. Havelund

    FM 2011.
    Lecture Notes in Computer Science, vol. 6664.
    pdf

  • Aspect-Oriented Instrumentation with GCC
    J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund, S. A. Smolka, S. D. Stoller, and E. Zadok

    The 1st International Conference on Runtime Verification (RV 2010)
    St. Julians, Malta, November 1-4, 2010.
    Lecture Notes in Computer Science, Vol. 6418.
    pdf

  • 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, Volume 7 - Issue 11, 2010.
    Invited talk given at the SMC-IT workshop: Software Reliability for Space Missions. July 20, 2009, Pasadena, California, USA.
    pdf

  • 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, Volume 7 - Issue 11, 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

  • From Scripts to Specifications - the Evolution of a Flight Software Testing Effort
    A. Groce, K. Havelund, and M. Smith

    ICSE '10 Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ACM New York, NY, USA 2010. doi 10.1145/1810295.1810314.
    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 Multithreaded 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, Volume: 54 Issue:5. September 2010.
    pdf

  • 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

    Annals of Mathematics and Artificial Intelligence.
    To appear.
    pdf

  • Requirements Capture with RCAT
    M. Smith and K. Havelund

    16th IEEE International Requirements Engineering Conference
    Barcelona, Spain, September 8-12, 2008.
    pdf

  • Aspect-Oriented Race Detection in Java
    E. Bodden and K. Havelund

    IEEE Transactions on Software Engineering, Volume 36 no. 4, July/August 2010 (invited journal version of ISSTA'08 paper). doi: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.25.
    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), Vol. 20 No. 3. Oxford University Press.
    Published online 21 November 2008 doi:10.1093/logcom/exn076.
    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

    WODA'05 Proceedings of the third international workshop on Dynamic analysis.
    St. Louis, Missouri, USA, May 17, 2005.
    ACM SIGSOFT Software Engineering Notes Volume 30 Issue 4, July 2005. ACM New York, NY, USA. doi: 10.1145/1083246.1083249.
    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
    pdf

  • 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
    pdf
    Won the ASE 2014 Most Influential Paper award: see MIP

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


JPL Java Coding Standard

JPL Institutional Coding Standard for the Java Programming Language.
Version 1.0, March 31, 2014.
Created by semmle.com, Klaus Havelund (JPL), and Al Niessner (JPL).
pdf

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

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

    An early version of the book is the RSL tutorial (draft) below (April 6, 1990).


Unpublished White Papers

  • Combining Modeling and Programming - Towards Advanced Languages for Software Development
    Manfred Broy and Klaus Havelund

    May 2015.
    pdf


The RAISE Project

The RAISE Esprit project (1984-1991), of which I was part, developed the specification language RSL (RAISE Specification Language), as well as a refinement-based method and tools, such as editors, type checkers, and proof tools. I was part of the 5 year language design effort, including writing dynamic semantics. The language was supposed to be a derivative of VDM, but took a completely different turn, combining algebraic specification with model-based specification, and a process specification language inspired by CCS and CSP. The contributors to the language were many over a more than 5 year period. Those that lastet to the end were Dines Bjoerner, 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.

This project was a lot of fun and we studied a lot of specification languages and semantics papers. Doing specification language design for 5 years does create a desire for experiencing/designing? the perfect programming language, a thought I have not yet given up. I claim that such a language does exist, and it is not far removed from those old specification languages. Scala is an excellent example.

The following reports are early and not quite complete versions of an RSL tutorial (which I wrote) and an RSL reference manual (which I wrote the dynamic semantics part of, while Anne Haxthausen wrote the static semantics/wellformedness part).
  • An RSL Tutorial
    K. Havelund
    Technical Report, Version 1, April 6, 1990
    Computer Resources International A/S.
    pdf

  • An RSL Reference Manual
    K. Havelund and A. Haxthausen
    Technical Report, Version 1, April 6, 1990
    Computer Resources International A/S.
    pdf



In addition I co-authored numerous Raise reports, which unfortunately seem to have gone lost.

RAISE website

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 More Technical Reports

  • Toward Automated Enforcement of Error-Handling Policies
    D. Smith and K. Havelund
    Technical Report number: TR-KT-0508, Kestrel Technology LLC. August 2005.
    pdf

  • 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

Free website templates