LTL satisfiability checking. - Kristin Y. Rozier; Moshe Y. Vardi (Int. J. Softw. Tools Technol. Transf., 2010)

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. - Kristin Y. Rozier; Moshe Y. Vardi (FM, 2011)

Linear Temporal Logic Symbolic Model Checking. - Kristin Y. Rozier (Comput. Sci. Rev., 2011)

Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking. - Kristin Yvonne Rozier; Moshe Y. Vardi (Haifa Verification Conference, 2012)

Optimized temporal monitors for SystemC. - Deian Tabakov; Kristin Y. Rozier; Moshe Y. Vardi (Formal Methods Syst. Des., 2012)

Probabilistic model checking for comparative analysis of automated air traffic control systems. - Yang Zhao; Kristin Y. Rozier (ICCAD, 2014)

Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems. - Johannes Geist; Kristin Y. Rozier; Johann Schumann (RV, 2014)

Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems. - Thomas Reinbacher; Kristin Yvonne Rozier; Johann Schumann (TACAS, 2014)

Formal specification and verification of a coordination protocol for an automated air traffic control system. - Yang Zhao; Kristin Yvonne Rozier (Sci. Comput. Program., 2014)

Comparing Different Functional Allocations in Automated Air Traffic Control Design. - Cristian Mattarei; Alessandro Cimatti; Marco Gario; Stefano Tonetta; Kristin Y. Rozier (FMCAD, 2015)

Characterizing Data Dependence Constraints for Dynamic Reliability Using N-Queens Attack Domains. - Ulya Bayram; Kristin Yvonne Rozier; Eric William Davis Rozier (QEST, 2015)

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. - Marco Gario; Alessandro Cimatti; Cristian Mattarei; Stefano Tonetta; Kristin Yvonne Rozier (CAV (2), 2016)

Cascading Solution to Data Dependence Constraints with Z3. - Eric William Davis Rozier; Kristin Y. Rozier (ISAIM, 2016)

Runtime Analysis with R2U2: A Tool Exhibition Report. - Johann Schumann; Patrick Moosbrugger; Kristin Y. Rozier (RV, 2016)

Specification: The Biggest Bottleneck in Formal Methods and Autonomy. - Kristin Yvonne Rozier (VSTTE, 2016)

FuseIC3: An algorithm for checking large design spaces. - Rohit Dureja; Kristin Yvonne Rozier (FMCAD, 2017)

On the Evaluation and Comparison of Runtime Verification Tools for Hardware and Cyber-Physical Systems. - Kristin Yvonne Rozier (RV-CuBES, 2017)

R2U2: Tool Overview. - Kristin Yvonne Rozier; Johann Schumann (RV-CuBES, 2017)

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. - Patrick Moosbrugger; Kristin Y. Rozier; Johann Schumann (Formal Methods Syst. Des., 2017)

Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains. - Eric William Davis Rozier; Kristin Y. Rozier; Ulya Bayram (Leibniz Trans. Embed. Syst., 2017)

SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. - Jianwen Li; Rohit Dureja; Geguang Pu; Kristin Yvonne Rozier; Moshe Y. Vardi (CAV (2), 2018)

A Broader View on Verification: From Static to Runtime and Back (Track Summary). - Wolfgang Ahrendt; Marieke Huisman; Giles Reger; Kristin Yvonne Rozier (ISoLA (2), 2018)

MLTL Benchmark Generation via Formula Progression. - Jianwen Li; Kristin Y. Rozier (RV, 2018)

More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 ). - Rohit Dureja; Kristin Yvonne Rozier (TACAS (1), 2018)

Satisfiability Checking for Mission-Time LTL. - Jianwen Li; Moshe Y. Vardi; Kristin Y. Rozier (CAV (2), 2019)

Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties. - Rohit Dureja; Jason Baumgartner; Alexander Ivrii; Robert Kanzelman; Kristin Y. Rozier (FMCAD, 2019)

From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques. - Kristin Yvonne Rozier (SpringSim, 2019)

On Teaching Applied Formal Methods in Aerospace Engineering. - Kristin Yvonne Rozier (FMTea, 2019)

Intersection and Rotation of Assumption Literals Boosts Bug-Finding. - Rohit Dureja; Jianwen Li; Geguang Pu; Moshe Y. Vardi; Kristin Y. Rozier (VSTTE, 2019)

Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. - Rohit Dureja; Jason Baumgartner; Robert Kanzelman; Mark Williams; Kristin Y. Rozier (FMCAD, 2020)

Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. - Brian Kempa; Pei Zhang 009; Phillip H. Jones; Joseph Zambreno; Kristin Yvonne Rozier (FORMATS, 2020)

SAT-based explicit LTLf satisfiability checking. - Jianwen Li; Geguang Pu; Yueling Zhang; Moshe Y. Vardi; Kristin Y. Rozier (Artif. Intell., 2020)

Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks. - Rohit Dureja; Kristin Yvonne Rozier (J. Aerosp. Inf. Syst., 2020)

Summarising a Framework for the Certification of Reliable Autonomous Systems. - Michael Fisher 001; Viviana Mascardi; Kristin Y. Rozier; Bernd-Holger Schlingloff; Michael Winikoff; Neil Yorke-Smith (AAMAS, 2021)

Integrating Runtime Verification into a Sounding Rocket Control System. - Benjamin Hertz; Zachary Luppen; Kristin Yvonne Rozier (NFM, 2021)

Towards a framework for certification of reliable autonomous systems. - Michael Fisher 001; Viviana Mascardi; Kristin Yvonne Rozier; Bernd-Holger Schlingloff; Michael Winikoff; Neil Yorke-Smith (Auton. Agents Multi Agent Syst., 2021)

Incremental design-space model checking via reusable reachable state approximations. - Rohit Dureja; Kristin Y. Rozier (Formal Methods Syst. Des., 2021)

MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types. - Gokul Hariharan; Brian Kempa; Tichakorn Wongpiromsarn; Phillip H. Jones; Kristin Y. Rozier (NSV/FoMLAS@CAV, 2022)

Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas. - Orion Staskal; Josh Simac; Logan Swayne; Kristin Y. Rozier (COMPSAC, 2022)

Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I. - Alexis A. Aurandt; Phillip H. Jones; Kristin Yvonne Rozier (NFM, 2022)

Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry. - Zachary Luppen; Michael Jacks; Nathan Baughman; Muhamed Stilic; Ryan Nasers; Benjamin Hertz; James W. Cutler; Dae Young Lee; Kristin Yvonne Rozier (NFM, 2022)

Satisfiability checking for Mission-time LTL (MLTL). - Jianwen Li; Moshe Y. Vardi; Kristin Y. Rozier (Inf. Comput., 2022)

Integrating runtime verification into an automated UAS traffic management system. - Abigail Hammer; Matthew Cauwels; Benjamin Hertz; Phillip H. Jones; Kristin Y. Rozier (Innov. Syst. Softw. Eng., 2022)

Threatpost Attack Stories 2021 (TAS21). - Megan K. Ryan; Kristin Yvonne Rozier (IEEE DataPort, 2022)

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; Phillip H. Jones; Brian Kempa; Kristin Yvonne Rozier; Pei Zhang 009 (CAV (3), 2023)

Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. - Kristin Y. Rozier; Natarajan Shankar; Cesare Tinelli; Moshe Y. Vardi (FMCAD, 2023)

Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints. - Chris Johannsen; Brian Kempa; Phillip H. Jones; Kristin Y. Rozier; Tichakorn Wongpiromsarn (FMICS, 2023)

Maximum Satisfiability of Mission-Time Linear Temporal Logic. - Gokul Hariharan; Phillip H. Jones; Kristin Yvonne Rozier; Tichakorn Wongpiromsarn (FORMATS, 2023)

Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines. - Pei Zhang 009; Alexis A. Aurandt; Rohit Dureja; Phillip H. Jones; Kristin Yvonne Rozier (FORMATS, 2023)

Mission-Time LTL (MLTL) Formula Validation via Regular Expressions. - Jenna Elwing; Laura P. Gamboa Guzman; Jeremy Sorkin; Chiara Travesset; Zili Wang 004; Kristin Yvonne Rozier (iFM, 2023)

What's in a Name? Linear Temporal Logic Literally Represents Time Lines. - Runming Li; Keerthana Gurushankar; Marijn J. H. Heule; Kristin Yvonne Rozier (VISSOFT, 2023)

Stalnaker's Epistemic Logic in Isabelle/HOL. - Laura P. Gamboa Guzman; Kristin Y. Rozier (LSFA/HCVS, 2023)

Model Learning for Improved Trustworthiness in Autonomous Systems (Dagstuhl Seminar 23492). - Ellen Enkel; Nils Jansen 001; Mohammad Reza Mousavi 001; Kristin Yvonne Rozier (Dagstuhl Reports, 2023)

The MoXI Model Exchange Tool Suite. - Chris Johannsen; Karthik Nukala; Rohit Dureja; Ahmed Irfan; Natarajan Shankar; Cesare Tinelli; Moshe Y. Vardi; Kristin Yvonne Rozier (CAV (1), 2024)

Toward Exhaustive Sequential Redundancy Removal. - Rohit Dureja; Jason Baumgartner; Raj Kumar Gajavelly; Robert Kanzelman; Kristin Y. Rozier (FMCAD, 2024)

Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems. - Alexis A. Aurandt; Phillip H. Jones; Kristin Yvonne Rozier; Tichakorn Wongpiromsarn (FMICS, 2024)

Formalizing Coppersmith's Method in Isabelle/HOL. - Katherine Kosaian; Yong Kiam Tan; Kristin Yvonne Rozier (CICM, 2024)

MoXI: An Intermediate Language for Symbolic Model Checking. - Kristin Yvonne Rozier; Rohit Dureja; Ahmed Irfan; Chris Johannsen; Karthik Nukala; Natarajan Shankar; Cesare Tinelli; Moshe Y. Vardi (SPIN, 2024)

R2U2: Runtime Verification Takes Off! (Keynote). - Kristin Yvonne Rozier (VORTEX@ISSTA, 2024)

Formalizing MLTL Formula Progression in Isabelle/HOL. - Katherine Kosaian; Zili Wang 004; Elizabeth Sloan; Kristin Y. Rozier (CoRR, 2024)

Infinite-State Liveness Checking with rlive. - Alessandro Cimatti; Alberto Griggio; Christopher Johannsen; Kristin Yvonne Rozier; Stefano Tonetta (CAV (1), 2025)

Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust. - Alexis A. Aurandt; Phillip H. Jones; Kristin Yvonne Rozier (NFM, 2025)

Language Partitioning for Mission-Time Linear Temporal Logic. - Alec Rosentrater; Zili Wang 004; Katherine Kosaian; Kristin Yvonne Rozier (NFM, 2025)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions. - Zili Wang 004; Katherine Kosaian; Kristin Yvonne Rozier (TACAS (1), 2025)

Formal Methods in Industry. - Maurice H. ter Beek; Rod Chapman; Rance Cleaveland; Hubert Garavel; Rong Gu; Ivo ter Horst; Jeroen J. A. Keiren; Thierry Lecomte; Michael Leuschel; Kristin Yvonne Rozier; Augusto Sampaio 001; Cristina Seceleanu; et al. (Formal Aspects Comput., 2025)

Neurosymbolic Feature Extraction for Identifying Forced Labor in Supply Chains. - Zili Wang 004; Frank Montabon; Kristin Yvonne Rozier (CoRR, 2025)

WEST: Interactive validation of Mission-time Linear Temporal Logic (MLTL). - Zili Wang 004; Laura P. Gamboa Guzman; Kristin Y. Rozier (Sci. Comput. Program., 2026)