Publications

1. From Natural Language Requirements to Runtime Monitors for Resource-Constrained Systems: Integrating FRET and R2U2

   Alexis Aurandt, Christopher Johannsen, Andreas Katis, Anastasia Mavridou, Kristin Yvonne Rozier, and Phillip H. Jones

   NASA Formal Methods (NFM), 2026

   PDF BibTeX
2. CTL Model Checking Partially Specified Systems

   Eshita Zaman, Christopher Johannsen, Andrew S. Miner, Gianfranco Ciardo, and Samik Basu

   Integrated Formal Methods (iFM), 2025

   PDF BibTeX
3. Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding

   Christopher Johannsen, Phillip H. Jones, Kristin Yvonne Rozier, and Tichakorn Wongpiromsarn

   Formal Methods in Computer Aided Design (FMCAD), 2025

   PDF Slides Artifact GitHub BibTeX
4. Infinite-state Liveness Checking with rlive

   Alessandro Cimatti, Alberto Griggio, Christopher Johannsen, Kristin Yvonne Rozier, and Stefano Tonetta

   International Conference on Computer Aided Verification (CAV), 2025

   PDF Slides Artifact BibTeX
5. The MoXI Model Exchange Tool Suite

   Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi and Kristin Yvonne Rozier

   International Conference on Computer Aided Verification (CAV), 2024

   PDF Slides GitHub Artifact BibTeX
6. MoXI: An Intermediate Language for Symbolic Model Checking

   Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli and Moshe Y. Vardi

   30th International Symposium on Model Checking Software (SPIN), 2024

   PDF Project Website GitHub Org. BibTeX
7. Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints

   Chris Johannsen, Brian Kempa, Phillip H Jones, Kristin Y Rozier, Tichakorn Wongpiromsarn

   International Conference on Formal Methods for Industrial Critical Systems (FMICS), 2023

   PDF Website Proofs Slides BibTeX
8. R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software

   Chris Johannsen, Brian Kempa, Phillip Jones, Kristin Yvonne Rozier, Pei Zhang

   International Conference on Computer Aided Verification (CAV), 2023

   PDF Website Slides Artifact BibTeX
9. Improving Usability and Trust in Real-Time Verification of a Large-Scale Complex Safety-Critical System

   Brian Kempa, Chris Johannsen, Kristin Yvonne Rozier

   Ada User Journal, Volume 43, Issue 3

   PDF Slides BibTeX
10. OpenUAS Version 1.0

    Chris Johannsen, Marcella Anderson, William Burken, Ellie Diersen, John Edgren, Colton Glick, Stephanie Jou, Adhyaksh Kumar, John Levandowski, Evelyn Moyer, Taylor Roquet, Alexander VandeLoo, Kristin Yvonne Rozier

    2021 International Conference on Unmanned Aircraft Systems (ICUAS)

    PDF BibTeX

Theses

1. Dynamic Set Reasoning: Specifying and Optimizing Monitor Encodings

   Chris Johannsen

   Masters Thesis, Iowa State University, 2024

   PDF Slides BibTeX