Klaus Havelund

Orcid: 0000-0001-7079-0472

Affiliations:
  • NASA Jet Propulsion Laboratory, Pasadena, CA, USA


According to our database1, Klaus Havelund authored at least 138 papers between 1989 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
High-Integrity Runtime Verification.
Computer, April, 2024

Programming event monitors.
Int. J. Softw. Tools Technol. Transf., February, 2024

TP-DejaVu: Combining Operational and Declarative Runtime Verification.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

2023
Concurrent runtime verification of data rich events.
Int. J. Softw. Tools Technol. Transf., August, 2023

AI Assisted Programming - (AISoLA 2023 Track Introduction).
Proceedings of the Bridging the Gap Between AI and Reality, 2023

Monitorability for Runtime Verification.
Proceedings of the Runtime Verification - 23rd International Conference, 2023

Space Telemetry Analysis with PyContract.
Proceedings of the Applicable Formal Methods for Safe Industrial Products, 2023

2022
On monitoring linear temporal properties.
Formal Methods Syst. Des., 2022

A Python Library for Trace Analysis.
Proceedings of the Runtime Verification - 22nd International Conference, 2022

Discussing the Future Role of Documentation in the Context of Modern Software Engineering (ISoLA 2022 Track Introduction).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

Specification-Based Monitoring in C++.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Runtime Verification as Documentation.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

2021
What can we monitor over unreliable channels?
Int. J. Softw. Tools Technol. Transf., 2021

An extension of first-order LTL with rules with application to runtime verification.
Int. J. Softw. Tools Technol. Transf., 2021

Monitoring First-Order Interval Logic.
Proceedings of the Software Engineering and Formal Methods - 19th International Conference, 2021

Programming - What is Next?
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 2021

Integrated Modeling and Development of Component-Based Embedded Software in Scala.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 2021

2020
First-order temporal logic monitoring with BDDs.
Formal Methods Syst. Des., 2020

Actor-Based Runtime Verification with MESA.
Proceedings of the Runtime Verification - 20th International Conference, 2020

BDDs for Representing Data in Runtime Verification.
Proceedings of the Runtime Verification - 20th International Conference, 2020

A Flight Rule Checker for the LADEE Lunar Spacecraft.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30, 2020

First-Order Timed Runtime Verification Using BDDs.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Runtime Verification Past Experiences and Future Projections.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

Introduction to Selected Papers from SPIN 2017.
Int. J. Softw. Tools Technol. Transf., 2019

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014.
Int. J. Softw. Tools Technol. Transf., 2019

Monitorability over Unreliable Channels.
Proceedings of the Runtime Verification - 19th International Conference, 2019

An Extension of LTL with Rules and Its Application to Runtime Verification.
Proceedings of the Runtime Verification - 19th International Conference, 2019

A Refinement Proof for a Garbage Collector.
Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

2018
Monitoring Events that Carry Data.
Proceedings of the Lectures on Runtime Verification - Introductory and Advanced Topics, 2018

Inferring event stream abstractions.
Formal Methods Syst. Des., 2018

Efficient Runtime Verification of First-Order Temporal Properties.
Proceedings of the Model Checking Software - 25th International Symposium, 2018

Runtime Verification - 17 Years Later.
Proceedings of the Runtime Verification - 18th International Conference, 2018

Runtime Verification: From Propositional to First-Order Temporal Logic.
Proceedings of the Runtime Verification - 18th International Conference, 2018

BDDs on the Run.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

Modeling with Scala.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

Towards a Unified View of Modeling and Programming (ISoLA 2018 Track Introduction).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

DejaVu: A Monitoring Tool for First-Order Temporal Logic.
Proceedings of the 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, 2018

Refining the Safety-Liveness Classification of Temporal Properties According to Monitorability.
Proceedings of the Models, Mindsets, 2018

2017
A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462).
Dagstuhl Reports, 2017

Modeling and Monitoring of Hierarchical State Machines in Scala.
Proceedings of the Software Engineering for Resilient Systems - 9th International Workshop, 2017

Modeling Rover Communication Using Hierarchical State Machines with Scala.
Proceedings of the Computer Safety, Reliability, and Security, 2017

Runtime Verification Logics A Language Design Perspective.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

2016
Some recent advances in automated analysis.
Int. J. Softw. Tools Technol. Transf., 2016

Verified Change.
LNCS Trans. Found. Mastering Chang., 2016

nfer - A Notation and System for Inferring Event Stream Abstractions.
Proceedings of the Runtime Verification - 16th International Conference, 2016

K: A Wide Spectrum Language for Modeling, Programming and Analysis.
Proceedings of the MODELSWARD 2016, 2016

What Is a Trace? A Runtime Verification Perspective.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Towards a Logic for Inferring Properties of Event Streams.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Static and Runtime Verification, Competitors or Friends? (Track Summary).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Towards a Unified View of Modeling and Programming (Track Summary).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Towards a Unified View of Modeling and Programming.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

2015
Rule-based runtime verification revisited.
Int. J. Softw. Tools Technol. Transf., 2015

Specification of Parametric Monitors.
Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, 2015

Domain-Specific Languages with Scala.
Proceedings of the Formal Methods and Software Engineering, 2015

2014
Verification and validation meet planning and scheduling.
Int. J. Softw. Tools Technol. Transf., 2014

Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning.
Ann. Math. Artif. Intell., 2014

Data Automata in Scala.
Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

Monitoring with Data Automata.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior.
Proceedings of the Formal Methods and Software Engineering, 2014

Experience with Rule-Based Analysis of Spacecraft Logs.
Proceedings of the Formal Techniques for Safety-Critical Systems, 2014

40 Years of Formal Methods - Some Obstacles and Some Possibilities?
Proceedings of the FM 2014: Formal Methods, 2014

Closing the Gap Between Specification and Programming: VDM++ and Scala.
Proceedings of the HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, 2014

Howard Barringer: the Man who Invented the Past.
Proceedings of the HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, 2014

2013
A Tutorial on Runtime Verification.
Proceedings of the Engineering Dependable Software Systems, 2013

A Scala DSL for Rete-Based Runtime Verification.
Proceedings of the Runtime Verification - 4th International Conference, 2013

2012
Introduction to the special section on runtime verification.
Int. J. Softw. Tools Technol. Transf., 2012

InterAspect: aspect-oriented instrumentation with GCC.
Formal Methods Syst. Des., 2012

Requirements-Driven Log Analysis (Extended Abstract).
Proceedings of the Testing Software and Systems, 2012

What Does AI Have to Do with RV? - (Extended Abstract).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors.
Proceedings of the FM 2012: Formal Methods, 2012

2011
Runtime Verification with State Estimation.
Proceedings of the Runtime Verification - Second International Conference, 2011

Internal versus External DSLs for Trace Analysis - (Extended Abstract).
Proceedings of the Runtime Verification - Second International Conference, 2011

TraceContract: A Scala DSL for Trace Analysis.
Proceedings of the FM 2011: Formal Methods, 2011

Software certification: coding, code, and coders.
Proceedings of the 11th International Conference on Embedded Software, 2011

2010
Aspect-Oriented Race Detection in Java.
IEEE Trans. Software Eng., 2010

Rule Systems for Run-time Monitoring: from Eagle to RuleR.
J. Log. Comput., 2010

Prototyping a Domain-Specific Language for Monitor and Control Systems.
J. Aerosp. Comput. Inf. Commun., 2010

Formal Analysis of Log Files.
J. Aerosp. Comput. Inf. Commun., 2010

Detection of deadlock potentials in multithreaded programs.
IBM J. Res. Dev., 2010

Aspect-Oriented Instrumentation with GCC.
Proceedings of the Runtime Verification - First International Conference, 2010

From scripts to specifications: the evolution of a flight software testing effort.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

10451 Executive Summary - Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems.
Proceedings of the Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems, 07.11., 2010

10451 Abstracts Collection - Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems.
Proceedings of the Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems, 07.11., 2010

2009
An Entry Point for Formal Methods: Specification and Analysis of Event Logs
Proceedings of the Proceedings FM-09 Workshop on Formal Methods for Aerospace, 2009

Rule Systems for Runtime Verification: A Short Tutorial.
Proceedings of the Runtime Verification, 9th International Workshop, 2009

2008
Requirements Capture with RCAT.
Proceedings of the 16th IEEE International Requirements Engineering Conference, 2008

Runtime Verification of C Programs.
Proceedings of the Testing of Software and Communicating Systems, 2008

Automated Testing of Planning Models.
Proceedings of the Model Checking and Artificial Intelligence, 5th International Workshop, 2008

Racer: effective race detection using aspectj.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

2007
Towards a framework and a benchmark for testing tools for multi-threaded programs.
Concurr. Comput. Pract. Exp., 2007

Rule Systems for Run-Time Monitoring: From Eagleto RuleR.
Proceedings of the Runtime Verification, 7th International Workshop, 2007

07011 Abstracts Collection -- Runtime Verification.
Proceedings of the Runtime Verification, 02.01. - 06.01.2007, 2007

07011 Executive Summary -- Runtime Verification.
Proceedings of the Runtime Verification, 02.01. - 06.01.2007, 2007

Visualization of Concurrent Program Executions.
Proceedings of the 31st Annual International Computer Software and Applications Conference, 2007

2006
Confirmation of deadlock potentials detected by runtime analysis.
Proceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, 2006

2005
Combining test case generation and runtime verification.
Theor. Comput. Sci., 2005

Event-based runtime verification of java programs.
ACM SIGSOFT Softw. Eng. Notes, 2005

Foreword.
Formal Methods Syst. Des., 2005

Rewriting-Based Techniques for Runtime Verification.
Autom. Softw. Eng., 2005

Automated Runtime Verification with Eagle.
Proceedings of the Modelling, 2005

Verify Your Runs.
Proceedings of the Verified Software: Theories, 2005

Dynamic Deadlock Analysis of Multi-threaded Programs.
Proceedings of the Hardware and Software Verification and Testing, 2005

2004
Efficient monitoring of safety properties.
Int. J. Softw. Tools Technol. Transf., 2004

An Overview of the Runtime Verification Tool Java PathExplorer.
Formal Methods Syst. Des., 2004

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

Experimental Evaluation of Verification and Validation Tools on Martian Rover Software.
Formal Methods Syst. Des., 2004

Rule-Based Runtime Verification.
Proceedings of the Verification, 2004

Applying Jlint to Space Exploration Software.
Proceedings of the Verification, 2004

Program Monitoring with LTL in EAGLE.
Proceedings of the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004

Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003
High-level data races.
Softw. Test. Verification Reliab., 2003

Model Checking Programs.
Autom. Softw. Eng., 2003

Benchmark and Framework for Encouraging Research on Multi-Threaded Testing Tools .
Proceedings of the 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 2003

Experiments with Test Case Generation and Runtime Analysis.
Proceedings of the Abstract State Machines, 2003

2002
Program model checking as a new trend.
Int. J. Softw. Tools Technol. Transf., 2002

Synthesizing Monitors for Safety Properties.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

2001
Formal Analysis of a Space-Craft Controller Using SPIN.
IEEE Trans. Software Eng., 2001

Monitoring Java Programs with Java PathExplorer.
Proceedings of the Workshop on Runtime Verification, 2001

Preface.
Proceedings of the Workshop on Runtime Verification, 2001

Mapping Temporal Planning Constraints into Timed Automata.
Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001

Monitoring Programs Using Rewriting.
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

Automata-Based Verification of Temporal Properties on Running Programs.
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

2000
Model Checking JAVA Programs using JAVA PathFinder.
Int. J. Softw. Tools Technol. Transf., 2000

Using Runtime Analysis to Guide Model Checking of Java Programs.
Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

Model Checking Programs.
Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering, 2000

Verification of Plan Models Using UPPAAL.
Proceedings of the Formal Approaches to Agent-Based Systems, First International Workshop, 2000

1999
Applying Model Checking in Java Verification.
Proceedings of the Theoretical and Practical Aspects of SPIN Model Checking, 1999

Java PathFinder, A Translator from Java to Promela.
Proceedings of the Theoretical and Practical Aspects of SPIN Model Checking, 1999

Mechanical Verification of a Garbage Collector.
Proceedings of the Parallel and Distributed Processing, 1999

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL.
Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1997
Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL.
Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997

Declarative Specification of Software Architectures.
Proceedings of the 1997 International Conference on Automated Software Engineering, 1997

Verification and Validation of AI Systems that Control Deep-Space Spacecraft.
Proceedings of the Foundations of Intelligent Systems, 10th International Symposium, 1997

1996
Experiments in Theorem Proving and Model Checking for Protocol Verification.
Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

1994
The Fork Calculus.
Nord. J. Comput., 1994

A refinement logic for the fork calculus.
Proceedings of the Protocol Specification, 1994

1992
Formal, model-oriented software development methods: From VDM to ProCoS & from RAISE to LaCoS.
Future Gener. Comput. Syst., 1992

1989
The RAISE Language, Method and Tools.
Formal Aspects Comput., 1989


  Loading...