Undated / under review
Safe Planning and Scheduling: An SMT-Based Verification Approach
K. Havelund and A. Pinto
Under review.
Publications
Search by title, author, topic, or year. Switch to full paper text to search inside the PDFs.
202 entries
According to the Web
Papers Published or Submitted for Publication
2026
AI Assisted Programming (AISoLA 2026 Track Introduction)
W. Ahrendt, B. K. Aichernig, and K. Havelund
AISoLA 2026 AISoLA Track: AI Assisted Programming. 27-31 October, 2026 - Kos, Greece. pdf
2026
Monitoring LLM Conversations with First-Order Temporal Logic
I. Cohen, K. Havelund, M. Omer, and D. Peled
RV 2026 pdf
2026
DejaVuGuard: Runtime Verification of LLM Conversations with First-Order Temporal Logic
I. Cohen, K. Havelund, M. Omer, and D. Peled
RV 2026 Tool paper. pdf
2026
Temporal Guardrails for LLM Conversations: A Runtime Verification Framework
I. Cohen, K. Havelund, M. Omer, and D. Peled
SAIV 2026 3rd International Symposium on AI Verification, Lisbon, Portugal. LNCS, pp. 145-166, Springer. pdf
2025
LLM-Assisted Translation and Bounded Model Checking of Python Code
S. Shivaji, K. Havelund, N. Lobakhina, L. C. Cordeiro, and A. Pinto
AISoLA 2025 AISoLA Track: AI Assisted Programming. 1-5 November, 2025 - Rhodes, Greece. pdf
2026
An Engineering Life-Cycle Assurance Process for Autonomous Space Systems
A. Pinto, C. Wagner, K. Havelund, and N. Rouquette
IEEE Aerospace Conference 2026 March 7-14, 2026, Big Sky, Montana. pdf
2025
Fuzz Testing with Temporal Constraints
K. Havelund, T. Clark, and and V. Reddy
ICTAC 2025 22nd International Colloquium on Theoretical Aspects of Computing. 24-28 Nov. 2025, Marrakesh, Morocco. Invited paper (keynote) pdf
2025
From Natural Language to Monitors via LLM-Assisted Disambiguation
I. Cohen, K. Havelund, D. Peled, and Y. Goldberg
RV 2025 pdf
2025
The Power of Reframing: Using LLMs in Synthesizing RV Monitors
I. Cohen, K. Havelund, D. Peled, and Y. Goldberg.
In Bettina Könighofer and Hazem Torfah, editors, RV 2025 25th International Conference on Runtime Verification, September 15-19, 2025 - Graz, Austria, LNCS, pp. 202-212, Springer-Verlag. pdf
2025
DSLs for Runtime Verification
K. Havelund, M. Omer, and D. Peled.
In Bettina Könighofer and Hazem Torfah, editors, RV 2025 25nd International Conference on Runtime Verification, September 15-19, 2025 - Graz, Austria, LNCS TBD, Springer-Verlag. Tutorial pdf
2025
Embedding Monitoring of First-order Temporal Logic in a Programming Language
K. Havelund, M. Omer, and D. Peled.
In Nathalie Bertrand, Clemens Dubslaff, and Sascha Klüppelholz, editors, Principles of Formal Quantitative Analysis - Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday. 2025. LNCS 15760, Springer-Verlag. Invited paper pdf
2025
AI Assisted Programming (AISoLA 2025 Post-Proceedings Track Introduction)
W. Ahrendt, B. K. Aichernig, and K. Havelund
AISoLA 2025 AISoLA Track: AI Assisted Programming. 1-5 November, 2025 - Rhodes, Greece. Post-proceedings. pdf
2025
AI Assisted Programming (AISoLA 2025 Track Introduction)
W. Ahrendt, B. K. Aichernig, and K. Havelund
AISoLA 2025 AISoLA Track: AI Assisted Programming. 1-5 November, 2025 - Rhodes, Greece. LNCS To Appear. pdf
2024
Correct-ish by Design: From Upfront Verification to Continuous Monitoring of LLM Generated Code
B. Aichernig and K. Havelund.
ISoLA/AISoLA 2024 AISoLA Track: AI Assisted Programming. 27 October - 3 November, 2024 - Crete, Greece. LNCS. pdf
2025
Presentation Abstract: Runtime Verification Tools
S. Kauffman and K. Havelund.
RRRR 2025 RRRR 2025 - Fourth Workshop on Reproducibility and Replication of Research Results. May 3, 2025. Published on website only. pdf
2024
AI Assisted Programming (AISoLA 2024 Track Introduction)
W. Ahrendt, B. K. Aichernig, and K. Havelund
ISoLA/AISoLA 2024 AISoLA Track: AI Assisted Programming. 27 October - 3 November, 2024 - Crete, Greece. LNCS To Appear. pdf
2024
High-Integrity Runtime Verification
A. E. Goodloe and K. Havelund
Computer, vol. 57, no. 4, pp. 37-45, April 2024. pdf
Undated / under review
Operational and Declarative Runtime Verification (Keynote)
K. Havelund, M. Omer, and and D. Peled
VORTEX '24: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution, ACM.
Undated / under review
What Is a Garbage Collector? An Exercise in Compositional Refinement
K. Havelund and N. Shankar
The Practice of Formal Methods - Essays in Honour of Cliff Jones, Part I. LNCS Volume 14780 pdf
2024
Does Every Computer Scientist Need to Know Formal Methods?
M. Broy, A. D. Brucker, A. Fantechi, M. Gleirscher, K. Havelund, M. Kuppe, A. Mendes, A. Platzer, J. O. Ringert, and A. Sullivan.
Formal Aspects of Computing, Springer International, 2024. pdf
2022
Introduction to Selected Papers from NFM 2022
J. Deshmukh, K. Havelund, I. Perez.
Innovations in Systems and Software Engineering, a NASA journal , Special Issue on NASA Formal Methods 2022 (NFM'22). Appeared online 2024, to appear in print. pdf
2024
TP-DejaVu: Combining Operational and Declarative Runtime Verification
K. Havelund, P. Katsaros, M. Omer, D. Peled, and A. Temperekidis
VMCAI'24, 25th International Conference on Verification, Model Checking and Abstract Interpretation, January 15-16, London, UK, 2024. LNCS 14500, Part II, 249-263. pdf
2023
AI-Assisted Programming with Test-based Refinement
B. Aichernig and K. Havelund
ISoLA 2023 Bridging the Gap Between AI and Reality. Track: AI Assisted Programming. 23-28 October 2023 - Crete, Greece. Abstract occurred in 2023 meeting proceedings, LNCS 14380. The full paper here will appear in post-meeting LNCS proceedings. pdf
2023
AI Assisted Programming (AISoLA 2023 Track Introduction)
W. Ahrendt and K. Havelund
ISoLA 2023 Bridging the Gap Between AI and Reality. Track: AI Assisted Programming. 23-28 October 2023 - Crete, Greece. LNCS 14380. pdf
2023
Monitorability for Runtime Verification
K. Havelund and D. Peled.
In Panagiotis Katsaros and Laura Nenzi, editors, 23rd International Conference on Runtime Verification, October 3-6, 2023 - Thessaloniki, Greece, LNCS 14245, 447-460, Springer-Verlag. Tutorial pdf
2023
Autonomica: Ontological Modeling and Analysis of Autonomous Behavior
M. Elaasar, N. Rouquette, K. Havelund, M. Feather, S. Bandyopadhyay, and A. Candela.
33rd Annual INCOSE International Symposium, Honolulu, HI, USA, July 15-20, 2023. pdf
2023
Programming Event Monitors
K. Havelund and G. J. Holzmann.
International Journal on Software Tools for Technology Transfer (STTT), 26:33-47, 2023. Springer-Verlag. pdf
2023
Space Telemetry Analysis with PyContract
B. Duckett, K. Havelund, and L. Stewart.
In Anne E. Haxthausen, Wen-Ling Huang, and Markus Roggenbach, editors, JanFest 2023. Essays Dedicated to Jan Peleska on the Occasion of His 65th Birthday, March 3, 2023 - Bremen, Germany, LNCS 14165, Springer-Verlag. Invited paper pdf
2022
Runtime Verification as Documentation
D. Dams, K. Havelund, and S. Kauffman.
ISoLA 2022 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Programming What is Next: The Role of Documentation. 22-30 October 2022 - Rhodes, Greece. LNCS 13702. pdf
2022
Discussing the Future Role of Documentation in the Context of Modern Software Engineering (ISoLA 2022 Track Introduction)
K. Havelund, T. Tegeler, S. Smyth, and B. Steffen.
ISoLA 2022 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Programming What is Next: The Role of Documentation. 22-30 October 2022 - Rhodes, Greece. LNCS 13702. pdf
2022
Specification-based Monitoring in C++
K. Havelund.
ISoLA 2022 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Specify This - Bridging gaps between program specification paradigms. 22-30 October 2022 - Rhodes, Greece. LNCS 13701. Invited paper pdf Was also presented at VPT 2022 (as a technical report).
2022
A Python Library for Trace Analysis
D. Dams, K. Havelund, and S. Kauffman
RV 2022 22nd International Conference on Runtime Verification, 28-30 September 2022 - Tbilisi, Georgia. LNCS 13498, Springer-Verlag. pdf
2023
On Monitoring Linear Temporal Properties
K. Havelund and D. Peled
Formal Methods in System Design (FMSD). A special issue in memory of Ed Clarke. Volume 60, pages 405-425, 2023. Invited paper pdf
2022
A Half Century of Formal Methods
D. Bjoerner and K. Havelund.
August 2022 (unpublished). pdf
2023
Concurrent Runtime Verification of Data Rich Events
N. Shafiei, K. Havelund, and P. Mehlitz.
International Journal on Software Tools for Technology Transfer (STTT), Volume 25, pages 481-501, 2023. Springer-Verlag. Journal version of RV 2020 paper. pdf
2021
Monitoring First-Order Interval Logic
K. Havelund, M. Omer, and D. Peled.
SEFM 2021 19th International Conference on Software Engineering and Formal Methods, 6-10 December 2021 - Jointly organised in virtual mode by Carnegie Mellon University (US), Nazarbayev University (Kazakhstan) and University of York (UK). pdf
2021
Programming - What is Next?
K. Havelund and B. Steffen.
ISoLA 2021 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Programming - What is Next? 25-29 October 2021 - Rhodes, Greece. LNCS 13036. pdf
2021
Integrated Modeling and Development of Component-Based Embedded Software in Scala
K. Havelund and R. Bocchino.
ISoLA 2021 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Programming - What is Next? 25-29 October 2021 - Rhodes, Greece. LNCS 13036. pdf
2022
Assurance of Model-Based Autonomy for Robotic Space Missions
M. S. Feather, S. L. Cornford, and K. Havelund.
RAMS 2022 68th Annual Reliability and Maintainability Symposium January 24-27, 2022, Tucson, Arizona, USA. pdf
2021
Information-Driven and Risk-Bounded Autonomy for Scientist Avatars
E. Timmons, M. Reeves, B. Ayton, B. C. Williams, M. D. Ingham, J. Castillo-Rogez, W. Seto, K. Havelund, A. Jasour, B. Donitz, D. Mages, A. Rahmani, P. Tavallali, and S. Chung.
ASCEND 2021 Organized by AIAA, Las Vegas, Nov 8-17, 2021. pdf
2021
An Extension of LTL with Rules and its Application to Runtime Verification
K. Havelund and D. Peled.
International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag. Issue 23/2021. pdf
2021
Towards a Systems Programming Language Designed for Hierarchical State Machines
B. McClelland, D. Tellier, M. Millman, K. Beatrix Go, A. Balayan, M. J. Munje, K. Dewey, N. Ho, K. Havelund, and M. Ingham.
SMC-IT 2021 8th IEEE International Conference on Space Mission Challenges for Information Technology. Online - July 26-30, 2021. pdf
2020
A Flight Rule Checker for the LADEE Lunar Spacecraft
E. Kurklu and K. Havelund.
ICTAC 2020 17th International Colloquium on Theoretical Aspects of Computing, 30 October - 4 Dec 2020 - Macau, China. LNCS TBD, Springer-Verlag. Keynote talk. pdf
2020
First-Order Timed Runtime Verification using BDDs
K. Havelund and D. Peled.
The 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20). Hanoi, Vietnam, October 19-23, 2020. Keynote talk. pdf
2020
Actor-based Runtime Verification with MESA
N. Shafiei, K. Havelund, and P. Mehlitz.
RV 2020 In Jyotirmoy Deshmukh and Dejan Nickovic, editors, 20th International Conference on Runtime Verification, 6-9 October 2020 - Los Angeles, USA. LNCS TBD, Springer-Verlag. (was one of three papers nominated for best paper award, but did not win it) pdf
2020
BDDs for Representing Data in Runtime Verification
K. Havelund and D. Peled.
RV 2020 In Jyotirmoy Deshmukh and Dejan Nickovic, editors, 20th International Conference on Runtime Verification, 6-9 October 2020 - Los Angeles, USA. LNCS TBD, Springer-Verlag. pdf
2021
What Can We Monitor Over Unreliable Channels?
S. Kauffman, K. Havelund, and S. Fischmeister.
International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag. Issue 23/2021. pdf
2019
An Extension of LTL with Rules and its Application to Runtime Verification
K. Havelund and D. Peled
RV 2019 In Bernd Finkbeiner and Leonardo Mariani, editors, 19th International Conference on Runtime Verification, 8-11 October 2019 - Porto, Portugal. LNCS TBD, Springer-Verlag. pdf
2019
Monitorability Over Unreliable Channels
S. Kauffman, K. Havelund, and S. Fischmeister
RV 2019 In Bernd Finkbeiner and Leonardo Mariani, editors, 19th International Conference on Runtime Verification, 8-11 October 2019 - Porto, Portugal. LNCS TBD, Springer-Verlag. pdf
2019
A Refinement Proof for a Garbage Collector
K. Havelund and N. Shankar.
In Ezio Bartocci, Rance Cleaveland, Radu Grosu, and Oleg Sokolsky, editors, ScottFest 2019 . Celebration of Scott Smolka's 65 year birthday, 1-2 August 2019 - Stony Brook, NY. LNCS TBD, Springer-Verlag. Invited presentation pdf
2018
Refining the Safety-liveness Classification of Temporal Properties According to Monitorability
D. Peled and K. Havelund
In Tiziana Margaria, Susanne Graf, and Kim Larsen, editors, Models, Mindsets, Meta - The What, The How, and the Why Not? Celebration of Berhard Steffen's 60 year birthday, 10-13 November 2018 - Limassol, Cyprus. LNCS 11200, Springer-Verlag. Invited presentation pdf Springer link
2019
Introduction to Selected Papers from SPIN 2017
H. Erdogmus and K. Havelund
International Journal on Software Tools for Technology Transfer (STTT), volume 21, 2019. Springer-Verlag. pdf Springer link
2018
The DejaVu Runtime Verification Benchmark
K. Havelund, D. Peled, and D. Ulus
RV 2018 18th International Conference on Runtime Verification, 10-13 November 2018 - Limassol, Cyprus. The RV RV competition . Published on website (not in LNCS proceedings). Won best benchmark price. pdf
2018
Runtime Verication - 17 Years Later
K. Havelund and G. Rosu
RV 2018 In Christian Columbo and Martin Leucker, editors, 18th International Conference on Runtime Verification, 10-13 November 2018 - Limassol, Cyprus. LNCS TBD, Springer-Verlag. Invited presentation in response to the authors receiving the 'Test of Time' award for their 2001 paper: Monitoring Java Programs with Java PathExplorer, RV'01, 2001. pdf
2018
Modeling with Scala
K. Havelund and R. Joshi
ISoLA 2018 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Towards a Unified View of Modeling and Programming. 5-9 November 2018 - Limasol, Cyprus. LNCS TBD, Springer-Verlag. pdf
2018
Towards a Unified View of Modeling and Programming (ISoLA 2018 Track Introduction)
M. Broy, K. Havelund, R. Kumar, B. Steffen.
ISoLA 2018 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Towards a Unified View of Modeling and Programming. 5-9 November 2018 - Limasol, Cyprus. LNCS TBD, Springer-Verlag. pdf
2018
Refining the Safety-liveness Classification of Temporal Properties According to Monitorability
D. Peled and K. Havelund
ISoLA 2018 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. 5-9 November 2018 - Limasol, Cyprus. LNCS TBD, Springer-Verlag. Invited presentation pdf --->
2018
Runtime Verification: From Propositional to First-Order Temporal Logic (Tutorial)
K. Havelund and D. Peled
RV 2018 In Christian Columbo and Martin Leucker, editors, 18th International Conference on Runtime Verification, 10-13 November 2018 - Limassol, Cyprus. LNCS TBD, Springer-Verlag. pdf
2018
BDDs on the Run
K. Havelund and D. Peled
ISoLA 2018 In Tiziana Margaria and Bernhard Steffen, editors, 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: RV-TheToP: Runtime Verification from the Theory To the industry Practice, organized by Ezio Bartocci and Ylies Falcone. 5-9 November 2018 - Limasol, Cyprus. LNCS TBD, Springer-Verlag. Invited presentation pdf
2018
Efficient Runtime Verification of First-Order Temporal Properties
K. Havelund and D. Peled
25th International Symposium on Model Checking of Software (SPIN 2018), 20-22 June, 2018, Malaga, Spain. LNCS Volume TBD. Invited presentation pdf
Undated / under review
Runtime Verification - Past Experiences and Future Projections
K. Havelund, G. Reger, and G. Rosu
LNCS 10000, special issue in celebration of issue number 10,000 of Lecture Notes in Computer Science. pdf Invited paper
2020
First-Order Temporal Logic Monitoring with BDDs
K. Havelund, D. Peled, and D. Ulus
Formal Methods in System Design (FMSD), 56, 1-21, 2020. Journal version of FMCAD 2017 paper with the same title. Springer link pdf
2018
DejaVu: A Monitoring Tool for First-Order Temporal Logic
K. Havelund, D. Peled, and D. Ulus
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS 2018), 10 April, 2018, Porto, Portugal. IEEE proceedings of CPSWEEK. pdf
2017
First Order Temporal Logic Monitoring with BDDs
K. Havelund, D. Peled, and D. Ulus
17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017), 2-6 October, 2017, Vienna, Austria. IEEE. pdf
2018
Inferring Event Stream Abstractions
S. Kauffman, K. Havelund, R. Joshi, and S. Fischmeister
Formal Methods in System Design (FMSD). Springer. 2018. Journal version of RV 2016 paper with the title: nfer - A Notation and System for Inferring Event Stream Abstractions. Online version pdf
2017
Modeling Rover Communication using Hierarchical State Machines with Scala
K. Havelund and R. Joshi
2nd International Workshop on the Timing Performance in Safety Engineering (TIPS 2017), 12 September, 2017, Trento, Italy. LNCS Volume TDB. pdf
2017
Modeling and Monitoring of Hierarchical State Machines in Scala
K. Havelund and R. Joshi
9th International Workshop on Software Engineering for Resilient Systems (SERENE 2017), September 4-5, 2017, Geneva, Switzerland. LNCS Volume TDB. pdf
2017
Runtime Verification Logics - A Language Design Perspective
K. Havelund and G. Reger
KIMfest 2017, a conference in honour of Kim G. Larsen on the occasion of his 60th birthday, 19-20 August 2017, Aalborg University, Denmark. LNCS TBD. pdf
2018
Monitoring Events that Carry Data
K. Havelund, G. Reger, D. Thoma, and E. Zalinescu
Book chapter in: Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS 10457, Springer. 2018. Book editors: Ezio Bartocci and Ylies Falcone. pdf
2017
First International Competition on Runtime Verification -- Rules, Benchmarks, Tools, and Final Results of CRV 2014
E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker, K. Havelund, Y. Joshi, F. Klaedtke, R. Milewicz, G. Reger, G. Rosu, J. Signoles, D. Thoma, E. Zalinescu, and Y. Zhang
International Journal on Software Tools for Technology Transfer (STTT), volume TDD, issue TDB, pages TBD, 2017. Springer-Verlag. online access pdf
2016
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
2016
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
2016
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
2016
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
2016
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
2016
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
2016
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. Pages 111-122. On short list of candidate papers to win the MODELSWARD 2016 best paper award. (but heck: did not make it). pdf NASA tech brief on The K Development Language.
2016
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
2016
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
2015
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
2015
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
2012
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
2014
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
2014
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
2014
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
2014
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
2014
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
2014
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
2014
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.
2013
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
2012
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
2012
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
2012
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
2012
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
2012
NASA Techbrief on LogScope and TraceContract
K. Havelund, M. Smith, H. Barringer, and A. Groce.
NTRS - NASA Technical Reports Server , August 2012, pdf
2012
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
2012
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
2011
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
2011
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
2011
Implementing Runtime Monitors
K. Havelund
TORRENTS 2011 2nd TORRENTS Workshop December 12, 2011, Toulouse, France. Invited presentation pdf
2011
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
2011
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
2011
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
2011
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
2011
TraceContract: A Scala DSL for Trace Analysis
H. Barringer and K. Havelund
FM 2011 . Lecture Notes in Computer Science, vol. 6664. pdf
2010
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
2010
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
2010
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
2010
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
2010
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
2010
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
2009
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
2009
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 )
Undated / under review
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
2008
Requirements Capture with RCAT
M. Smith and K. Havelund
16th IEEE International Requirements Engineering Conference Barcelona, Spain, September 8-12, 2008. pdf
2010
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
2008
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 )
2008
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
2008
Runtime Verification of C Programs
K. Havelund
TestCom/FATES conference Lecture Notes in Computer Science volume 5047. Tokyo, Japan, June 10-13, 2008. pdf
2008
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
2008
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
2007
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
2008
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
2007
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.
2006
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
2006
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
2005
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
2005
Verify Your Runs
K. Havelund and A. Goldberg
Verified Software: Theories, Tools, Experiments ( VSTTE'05 ) Zurich, Switzerland, October 10-13, 2005 pdf
2005
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
2005
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
2005
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
2005
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
2004
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
2004
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
2004
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
2004
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
Undated / under review
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
2003
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
2003
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
2003
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
2004
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
2003
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
2003
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
2005
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
2003
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
2002
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)
2002
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
2003
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
2002
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
2004
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
2002
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
2002
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
2004
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
2001
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
2001
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)
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
2004
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
2001
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 Won the RV 2018 Test of time award (most influential RV paper from 2001). ps , ps.gz
2001
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
2000
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
2003
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
2000
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 . Won the 2020 SIGSOFT Impact Paper Award!
2000
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
2001
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
2000
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
2000
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
1999
Adding Active Objects to SPIN
W. Visser, K. Havelund, J. Penix
Appeared in proceedings of 5th SPIN Workshop, July 1999, Trento ps , ps.Z
Undated / under review
Applying Model Checking in Java Verification
K. Havelund, J. Skakkebaek
Proceedings of 6th SPIN Workshop in connection with FM99 Toulouse ps , ps.Z
2000
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
1999
Java PathFinder, A Translator from Java to Promela
K. Havelund
Theoretical and Practical Aspects of SPIN Model Checking, Toulouse, France, September, 1999 pdf
2001
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)
Undated / under review
Mechanical Verification of a Garbage Collector
K. Havelund
FMPPTA'99 ps , ps.Z ps , ps.Z (Tech. report)
Undated / under review
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
Undated / under review
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)
Undated / under review
Using Model Checking to Validate AI Planner Domain Models
J. Penix, C. Pecheur, K. Havelund
SEL'98 ps , ps.Z
Undated / under review
Verification and Validation of AI Systems that Control Deep-Space Spacecrafts
M. Lowry, K. Havelund, J. Penix
ISMIS'97 ps , ps.Z
Undated / under review
Declarative Specification of Software Architectures
J. Penix, P. Alexander, K. Havelund
ASE'97 ps , ps.Z
Undated / under review
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
Undated / under review
Experiments in Theorem Proving and Model Checking
K. Havelund, N. Shankar
FME'96 ps , ps.Z ps , ps.Z (Tech. report)
Undated / under review
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)
Undated / under review
A Refinement Logic for the Fork Calculus
K. Havelund, K.G. Larsen
PSTV'94 ps , ps.Z
1992
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
1989
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
1988
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.
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.
An RSL Reference Manual
K. Havelund and A. Haxthausen
Technical Report, Version 1, April 6, 1990**
Computer Resources International A/S.
In addition I co-authored numerous Raise reports, which unfortunately seem to have gone lost.
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.
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.
Technical Reports
Empirical Study of Actor-based Runtime Verification
N. Shafiei, K. Havelund, and P. Mehlitz
NASA Technical Report number: NASA/TM-2020-5004331.
June 2020.
Also available at http://ntrs.nasa.gov
Toward Automated Enforcement of Error-Handling Policies
D. Smith and K. Havelund
Technical Report number: TR-KT-0508, Kestrel Technology LLC.
August 2005.
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.
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
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
pdf
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
pdf
Java PathFinder User Guide
K. Havelund
Unpublished Report
pdf
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
Unpublished Report, 1997
StateText - A Textual Language for State Charts with Data
K. Havelund, K. G. Larsen
Unpublished Report
pdf