The RAISE Language, Method and Tools. - Mogens Nielsen; Klaus Havelund; Kim Ritter Wagner; Chris George (Formal Aspects Comput., 1989)

Formal, model-oriented software development methods: From VDM to ProCoS & from RAISE to LaCoS. - Dines Bjørner; Anne Elisabeth Haxthausen; Klaus Havelund (Future Gener. Comput. Syst., 1992)

A refinement logic for the fork calculus. - Klaus Havelund; Kim Guldstrand Larsen (PSTV, 1994)

The Fork Calculus. - Klaus Havelund; Kim Guldstrand Larsen (Nord. J. Comput., 1994)

Experiments in Theorem Proving and Model Checking for Protocol Verification. - Klaus Havelund; Natarajan Shankar (FME, 1996)

Verification and Validation of AI Systems that Control Deep-Space Spacecraft. - Michael R. Lowry; Klaus Havelund; John Penix (ISMIS, 1997)

Declarative Specification of Software Architectures. - John Penix; Perry Alexander; Klaus Havelund (ASE, 1997)

Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL. - Klaus Havelund; Arne Skou; Kim Guldstrand Larsen; Kristian Lund (RTSS, 1997)

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL. - Klaus Havelund; Kim Guldstrand Larsen; Arne Skou (ARTS, 1999)

Mechanical Verification of a Garbage Collector. - Klaus Havelund (IPPS/SPDP Workshops, 1999)

Java PathFinder, A Translator from Java to Promela. - Klaus Havelund (SPIN, 1999)

Applying Model Checking in Java Verification. - Klaus Havelund; Jens U. Skakkebæk (SPIN, 1999)

Verification of Plan Models Using UPPAAL. - Lina Khatib; Nicola Muscettola; Klaus Havelund (FAABS, 2000)

Model Checking Programs. - Willem Visser; Klaus Havelund; Guillaume P. Brat; Seungjoon Park (ASE, 2000)

Using Runtime Analysis to Guide Model Checking of Java Programs. - Klaus Havelund (SPIN, 2000)

Model Checking JAVA Programs using JAVA PathFinder. - Klaus Havelund; Thomas Pressburger (Int. J. Softw. Tools Technol. Transf., 2000)

Automata-Based Verification of Temporal Properties on Running Programs. - Dimitra Giannakopoulou; Klaus Havelund (ASE, 2001)

Monitoring Programs Using Rewriting. - Klaus Havelund; Grigore Rosu (ASE, 2001)

Mapping Temporal Planning Constraints into Timed Automata. - Lina Khatib; Nicola Muscettola; Klaus Havelund (TIME, 2001)

Preface. - Klaus Havelund; Grigore Rosu (RV@CAV, 2001)

Monitoring Java Programs with Java PathExplorer. - Klaus Havelund; Grigore Rosu (RV@CAV, 2001)

Formal Analysis of a Space-Craft Controller Using SPIN. - Klaus Havelund; Michael R. Lowry; John Penix (IEEE Trans. Software Eng., 2001)

Synthesizing Monitors for Safety Properties. - Klaus Havelund; Grigore Rosu (TACAS, 2002)

Program model checking as a new trend. - Klaus Havelund; Willem Visser (Int. J. Softw. Tools Technol. Transf., 2002)

Experiments with Test Case Generation and Runtime Analysis. - Cyrille Artho; Doron Drusinsky; Allen Goldberg; Klaus Havelund; Michael R. Lowry; Corina S. Pasareanu; Grigore Rosu; Willem Visser (Abstract State Machines, 2003)

Benchmark and Framework for Encouraging Research on Multi-Threaded Testing Tools . - Klaus Havelund; Scott D. Stoller; Shmuel Ur (IPDPS, 2003)

Model Checking Programs. - Willem Visser; Klaus Havelund; Guillaume P. Brat; Seungjoon Park; Flavio Lerda (Autom. Softw. Eng., 2003)

High-level data races. - Cyrille Artho; Klaus Havelund; Armin Biere (Softw. Test. Verification Reliab., 2003)

Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. - Cyrille Artho; Klaus Havelund; Armin Biere (ATVA, 2004)

Program Monitoring with LTL in EAGLE. - Howard Barringer; Allen Goldberg; Klaus Havelund; Koushik Sen (IPDPS, 2004)

Applying Jlint to Space Exploration Software. - Cyrille Artho; Klaus Havelund (VMCAI, 2004)

Rule-Based Runtime Verification. - Howard Barringer; Allen Goldberg; Klaus Havelund; Koushik Sen (VMCAI, 2004)

Experimental Evaluation of Verification and Validation Tools on Martian Rover Software. - Guillaume P. Brat; Doron Drusinsky; Dimitra Giannakopoulou; Allen Goldberg; Klaus Havelund; Michael R. Lowry; Corina S. Pasareanu; Arnaud Venet; Willem Visser; Richard Washington (Formal Methods Syst. Des., 2004)

Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01). - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2004)

An Overview of the Runtime Verification Tool Java PathExplorer. - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2004)

Efficient monitoring of safety properties. - Klaus Havelund; Grigore Rosu (Int. J. Softw. Tools Technol. Transf., 2004)

Dynamic Deadlock Analysis of Multi-threaded Programs. - Saddek Bensalem; Klaus Havelund (Haifa Verification Conference, 2005)

Verify Your Runs. - Klaus Havelund; Allen Goldberg (VSTTE, 2005)

Automated Runtime Verification with Eagle. - Allen Goldberg; Klaus Havelund (MSVVEIS, 2005)

Rewriting-Based Techniques for Runtime Verification. - Grigore Rosu; Klaus Havelund (Autom. Softw. Eng., 2005)

Foreword. - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2005)

Event-based runtime verification of java programs. - Marcelo d'Amorim; Klaus Havelund (ACM SIGSOFT Softw. Eng. Notes, 2005)

Combining test case generation and runtime verification. - Cyrille Artho; Howard Barringer; Allen Goldberg; Klaus Havelund; Sarfraz Khurshid; Michael R. Lowry; Corina S. Pasareanu; Grigore Rosu; Koushik Sen; Willem Visser; Richard Washington (Theor. Comput. Sci., 2005)

Confirmation of deadlock potentials detected by runtime analysis. - Saddek Bensalem; Jean-Claude Fernandez; Klaus Havelund; Laurent Mounier (PADTAD, 2006)

Visualization of Concurrent Program Executions. - Cyrille Artho; Klaus Havelund; Shinichi Honiden (COMPSAC (2), 2007)

07011 Executive Summary – Runtime Verification. - Bernd Finkbeiner; Klaus Havelund; Grigore Rosu; Oleg Sokolsky (Runtime Verification, 2007)

07011 Abstracts Collection – Runtime Verification. - Bernd Finkbeiner; Klaus Havelund; Grigore Rosu; Oleg Sokolsky (Runtime Verification, 2007)

Rule Systems for Run-Time Monitoring: From Eagleto RuleR. - Howard Barringer; David E. Rydeheard; Klaus Havelund (RV, 2007)

Towards a framework and a benchmark for testing tools for multi-threaded programs. - Yaniv Eytani; Klaus Havelund; Scott D. Stoller; Shmuel Ur (Concurr. Comput. Pract. Exp., 2007)

Racer: effective race detection using aspectj. - Eric Bodden; Klaus Havelund (ISSTA, 2008)

Automated Testing of Planning Models. - Klaus Havelund; Alex Groce; Gerard J. Holzmann; Rajeev Joshi; Margaret H. Smith (MoChArt, 2008)

Runtime Verification of C Programs. - Klaus Havelund (TestCom/FATES, 2008)

Requirements Capture with RCAT. - Margaret H. Smith; Klaus Havelund (RE, 2008)

Rule Systems for Runtime Verification: A Short Tutorial. - Howard Barringer; Klaus Havelund; David E. Rydeheard; Alex Groce (RV, 2009)

An Entry Point for Formal Methods: Specification and Analysis of Event Logs - Howard Barringer; Alex Groce; Klaus Havelund; Margaret H. Smith (FMA, 2009)

10451 Abstracts Collection - Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. - Klaus Havelund; Martin Leucker; Martin Sachenbacher; Oleg Sokolsky; Brian C. Williams (Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems, 2010)

10451 Executive Summary - Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. - Klaus Havelund; Martin Leucker; Martin Sachenbacher; Oleg Sokolsky; Brian C. Williams (Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems, 2010)

From scripts to specifications: the evolution of a flight software testing effort. - Alex Groce; Klaus Havelund; Margaret H. Smith (ICSE (2), 2010)

Aspect-Oriented Instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (RV, 2010)

Detection of deadlock potentials in multithreaded programs. - Rahul Agarwal; Saddek Bensalem; Eitan Farchi; Klaus Havelund; Yarden Nir-Buchbinder; Scott D. Stoller; Shmuel Ur; Liqiang Wang (IBM J. Res. Dev., 2010)

Formal Analysis of Log Files. - Howard Barringer; Alex Groce; Klaus Havelund; Margaret H. Smith (J. Aerosp. Comput. Inf. Commun., 2010)

Prototyping a Domain-Specific Language for Monitor and Control Systems. - Matthew Bennett; Richard Borgen; Klaus Havelund; Michel D. Ingham; David A. Wagner 002 (J. Aerosp. Comput. Inf. Commun., 2010)

Rule Systems for Run-time Monitoring: from Eagle to RuleR. - Howard Barringer; David E. Rydeheard; Klaus Havelund (J. Log. Comput., 2010)

Aspect-Oriented Race Detection in Java. - Eric Bodden; Klaus Havelund (IEEE Trans. Software Eng., 2010)

Software certification: coding, code, and coders. - Klaus Havelund; Gerard J. Holzmann (EMSOFT, 2011)

TraceContract: A Scala DSL for Trace Analysis. - Howard Barringer; Klaus Havelund (FM, 2011)

Internal versus External DSLs for Trace Analysis - (Extended Abstract). - Howard Barringer; Klaus Havelund (RV, 2011)

Runtime Verification with State Estimation. - Scott D. Stoller; Ezio Bartocci; Justin Seyster; Radu Grosu; Klaus Havelund; Scott A. Smolka; Erez Zadok (RV, 2011)

Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. - Howard Barringer; Yliès Falcone; Klaus Havelund; Giles Reger; David E. Rydeheard (FM, 2012)

What Does AI Have to Do with RV? - (Extended Abstract). - Klaus Havelund (ISoLA (1), 2012)

Requirements-Driven Log Analysis (Extended Abstract). - Klaus Havelund (ICTSS, 2012)

InterAspect: aspect-oriented instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (Formal Methods Syst. Des., 2012)

Introduction to the special section on runtime verification. - Oleg Sokolsky; Klaus Havelund; Insup Lee 001 (Int. J. Softw. Tools Technol. Transf., 2012)

A Scala DSL for Rete-Based Runtime Verification. - Klaus Havelund (RV, 2013)

A Tutorial on Runtime Verification. - Yliès Falcone; Klaus Havelund; Giles Reger (Engineering Dependable Software Systems, 2013)

Howard Barringer: the Man who Invented the Past. - Klaus Havelund (HOWARD-60, 2014)

Closing the Gap Between Specification and Programming: VDM++ and Scala. - Klaus Havelund (HOWARD-60, 2014)

40 Years of Formal Methods - Some Obstacles and Some Possibilities? - Dines Bjørner; Klaus Havelund (FM, 2014)

Experience with Rule-Based Analysis of Spacecraft Logs. - Klaus Havelund; Rajeev Joshi (FTSCS, 2014)

Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior. - Klaus Havelund; Rajeev Joshi (ICFEM, 2014)

Monitoring with Data Automata. - Klaus Havelund (ISoLA (2), 2014)

Data Automata in Scala. - Klaus Havelund (TASE, 2014)

Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning. - Alex Groce; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi; Ru-Gang Xu (Ann. Math. Artif. Intell., 2014)

Verification and validation meet planning and scheduling. - Saddek Bensalem; Klaus Havelund; Andrea Orlandini (Int. J. Softw. Tools Technol. Transf., 2014)

Domain-Specific Languages with Scala. - Cyrille Artho; Klaus Havelund; Rahul Kumar 001; Yoriyuki Yamagata (ICFEM, 2015)

Specification of Parametric Monitors. - Klaus Havelund; Giles Reger (SyDe Summer School, 2015)

Rule-based runtime verification revisited. - Klaus Havelund (Int. J. Softw. Tools Technol. Transf., 2015)

Towards a Unified View of Modeling and Programming. - Manfred Broy; Klaus Havelund; Rahul Kumar 001 (ISoLA (2), 2016)

Towards a Unified View of Modeling and Programming (Track Summary). - Manfred Broy; Klaus Havelund; Rahul Kumar 001; Bernhard Steffen (ISoLA (2), 2016)

Static and Runtime Verification, Competitors or Friends? (Track Summary). - Dilian Gurov; Klaus Havelund; Marieke Huisman; Rosemary Monahan (ISoLA (1), 2016)

Towards a Logic for Inferring Properties of Event Streams. - Sean Kauffman; Rajeev Joshi; Klaus Havelund (ISoLA (2), 2016)

What Is a Trace? A Runtime Verification Perspective. - Giles Reger; Klaus Havelund (ISoLA (2), 2016)

K: A Wide Spectrum Language for Modeling, Programming and Analysis. - Klaus Havelund; Rahul Kumar 001; Chris Delp; Bradley Clement (MODELSWARD, 2016)

nfer - A Notation and System for Inferring Event Stream Abstractions. - Sean Kauffman; Klaus Havelund; Rajeev Joshi (RV, 2016)

Verified Change. - Klaus Havelund; Rahul Kumar 001 (LNCS Trans. Found. Mastering Chang., 2016)

Some recent advances in automated analysis. - Erika Ábrahám; Klaus Havelund (Int. J. Softw. Tools Technol. Transf., 2016)

Runtime Verification Logics A Language Design Perspective. - Klaus Havelund; Giles Reger (Models, Algorithms, Logics and Tools, 2017)

Modeling Rover Communication Using Hierarchical State Machines with Scala. - Klaus Havelund; Rajeev Joshi (SAFECOMP Workshops, 2017)

Modeling and Monitoring of Hierarchical State Machines in Scala. - Klaus Havelund; Rajeev Joshi (SERENE, 2017)

A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462). - Klaus Havelund; Martin Leucker; Giles Reger; Volker Stolz (Dagstuhl Reports, 2017)

Refining the Safety-Liveness Classification of Temporal Properties According to Monitorability. - Doron Peled; Klaus Havelund (Models, Mindsets, Meta, 2018)

DejaVu: A Monitoring Tool for First-Order Temporal Logic. - Klaus Havelund; Doron Peled; Dogan Ulus (MT@CPSWeek, 2018)

Towards a Unified View of Modeling and Programming (ISoLA 2018 Track Introduction). - Manfred Broy; Klaus Havelund; Rahul Kumar 001; Bernhard Steffen (ISoLA (1), 2018)

Modeling with Scala. - Klaus Havelund; Rajeev Joshi (ISoLA (1), 2018)

BDDs on the Run. - Klaus Havelund; Doron Peled (ISoLA (4), 2018)

Runtime Verification: From Propositional to First-Order Temporal Logic. - Klaus Havelund; Doron Peled (RV, 2018)

Runtime Verification - 17 Years Later. - Klaus Havelund; Grigore Rosu (RV, 2018)

Efficient Runtime Verification of First-Order Temporal Properties. - Klaus Havelund; Doron Peled (SPIN, 2018)

Inferring event stream abstractions. - Sean Kauffman; Klaus Havelund; Rajeev Joshi; Sebastian Fischmeister (Formal Methods Syst. Des., 2018)

Monitoring Events that Carry Data. - Klaus Havelund; Giles Reger; Daniel Thoma; Eugen Zalinescu (Lectures on Runtime Verification, 2018)

A Refinement Proof for a Garbage Collector. - Klaus Havelund; Natarajan Shankar (From Reactive Systems to Cyber-Physical Systems, 2019)

An Extension of LTL with Rules and Its Application to Runtime Verification. - Klaus Havelund; Doron Peled (RV, 2019)

Monitorability over Unreliable Channels. - Sean Kauffman; Klaus Havelund; Sebastian Fischmeister (RV, 2019)

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. - Ezio Bartocci; Yliès Falcone; Borzoo Bonakdarpour; Christian Colombo 001; Normann Decker; Klaus Havelund; Yogi Joshi; Felix Klaedtke; Reed Milewicz; Giles Reger; Grigore Rosu; Julien Signoles; et al. (Int. J. Softw. Tools Technol. Transf., 2019)

Introduction to Selected Papers from SPIN 2017. - Hakan Erdogmus; Klaus Havelund (Int. J. Softw. Tools Technol. Transf., 2019)

Runtime Verification Past Experiences and Future Projections. - Klaus Havelund; Giles Reger; Grigore Rosu (Computing and Software Science, 2019)

First-Order Timed Runtime Verification Using BDDs. - Klaus Havelund; Doron Peled (ATVA, 2020)

A Flight Rule Checker for the LADEE Lunar Spacecraft. - Elif Kürklü; Klaus Havelund (ICTAC, 2020)

BDDs for Representing Data in Runtime Verification. - Klaus Havelund; Doron Peled (RV, 2020)

Actor-Based Runtime Verification with MESA. - Nastaran Shafiei; Klaus Havelund; Peter C. Mehlitz (RV, 2020)

First-order temporal logic monitoring with BDDs. - Klaus Havelund; Doron Peled; Dogan Ulus (Formal Methods Syst. Des., 2020)

Integrated Modeling and Development of Component-Based Embedded Software in Scala. - Klaus Havelund; Robert Bocchino (ISoLA, 2021)

Programming - What is Next? - Klaus Havelund; Bernhard Steffen (ISoLA, 2021)

Monitoring First-Order Interval Logic. - Klaus Havelund; Moran Omer; Doron Peled (SEFM, 2021)

An extension of first-order LTL with rules with application to runtime verification. - Klaus Havelund; Doron Peled (Int. J. Softw. Tools Technol. Transf., 2021)

What can we monitor over unreliable channels? - Sean Kauffman; Klaus Havelund; Sebastian Fischmeister (Int. J. Softw. Tools Technol. Transf., 2021)

Runtime Verification as Documentation. - Dennis Dams; Klaus Havelund; Sean Kauffman (ISoLA (2), 2022)

Specification-Based Monitoring in C++. - Klaus Havelund (ISoLA (1), 2022)

Discussing the Future Role of Documentation in the Context of Modern Software Engineering (ISoLA 2022 Track Introduction). - Klaus Havelund; Tim Tegeler; Steven Smyth; Bernhard Steffen (ISoLA (2), 2022)

A Python Library for Trace Analysis. - Dennis Dams; Klaus Havelund; Sean Kauffman (RV, 2022)

On monitoring linear temporal properties. - Klaus Havelund; Doron Peled (Formal Methods Syst. Des., 2022)

Space Telemetry Analysis with PyContract. - Bevin Duckett; Klaus Havelund; Luke Stewart (Applicable Formal Methods for Safe Industrial Products, 2023)

Monitorability for Runtime Verification. - Klaus Havelund; Doron Peled (RV, 2023)

AI Assisted Programming - (AISoLA 2023 Track Introduction). - Wolfgang Ahrendt; Klaus Havelund (AISoLA, 2023)

AI-Assisted Programming with Test-Based Refinement. - Bernhard K. Aichernig; Klaus Havelund (AISoLA (Selected Papers), 2023)

Concurrent runtime verification of data rich events. - Nastaran Shafiei; Klaus Havelund; Peter C. Mehlitz (Int. J. Softw. Tools Technol. Transf., 2023)

AI Assisted Programming - (AISoLA 2024 Track Introduction). - Wolfgang Ahrendt; Bernhard K. Aichernig; Klaus Havelund (AISoLA, 2024)

TP-DejaVu: Combining Operational and Declarative Runtime Verification. - Klaus Havelund; Panagiotis Katsaros; Moran Omer; Doron Peled; Anastasios Temperekidis (VMCAI (2), 2024)

Operational and Declarative Runtime Verification (Keynote). - Klaus Havelund; Moran Omer; Doron Peled (VORTEX@ISSTA, 2024)

What Is a Garbage Collector? An Exercise in Compositional Refinement. - Klaus Havelund; Natarajan Shankar (The Practice of Formal Methods (I), 2024)

Programming event monitors. - Klaus Havelund; Gerard J. Holzmann (Int. J. Softw. Tools Technol. Transf., 2024)

High-Integrity Runtime Verification. - Alwyn E. Goodloe; Klaus Havelund (Computer, 2024)

Does Every Computer Scientist Need to Know Formal Methods? - Manfred Broy; Achim D. Brucker; Alessandro Fantechi; Mario Gleirscher; Klaus Havelund; Markus Alexander Kuppe; Alexandra Mendes; André Platzer; Jan Oliver Ringert; Allison Sullivan (Formal Aspects Comput., 2025)