Kristin Y. Rozier

According to our database, Kristin Y. Rozier authored at least 59 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Formalizing MLTL Formula Progression in Isabelle/HOL.

Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Y. Rozier

CoRR, 2024

R2U2: Runtime Verification Takes Off! (Keynote).

Kristin Yvonne Rozier

Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution, 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

Proceedings of the Model Checking Software - 30th International Symposium, 2024

Formalizing Coppersmith's Method in Isabelle/HOL.

Katherine Kosaian, Yong Kiam Tan, Kristin Yvonne Rozier

Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems.

Alexis A. Aurandt, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn

Proceedings of the Formal Methods for Industrial Critical Systems, 2024

The MoXI Model Exchange Tool Suite.

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

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Model Learning for Improved Trustworthiness in Autonomous Systems (Dagstuhl Seminar 23492).

Ellen Enkel, Nils Jansen, Mohammad Reza Mousavi, Kristin Yvonne Rozier

Dagstuhl Reports, December, 2023

Stalnaker's Epistemic Logic in Isabelle/HOL.

Laura P. Gamboa Guzman, Kristin Y. Rozier

Proceedings of the Proceedings 18th International Workshop on Logical and Semantic Frameworks, 2023

What's in a Name? Linear Temporal Logic Literally Represents Time Lines.

Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier

Proceedings of the IEEE Working Conference on Software Visualization, 2023

Mission-Time LTL (MLTL) Formula Validation via Regular Expressions.

Jenna Elwing, Laura Gamboa-Guzman, Jeremy Sorkin, Chiara Travesset, Zili Wang, Kristin Yvonne Rozier

Proceedings of the iFM 2023 - 18th International Conference, 2023

Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines.

Pei Zhang, Alexis A. Aurandt, Rohit Dureja, Phillip H. Jones, Kristin Yvonne Rozier

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2023

Maximum Satisfiability of Mission-Time Linear Temporal Logic.

Gokul Hariharan, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2023

Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints.

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

Proceedings of the Formal Methods for Industrial Critical Systems, 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

Proceedings of the Formal Methods in Computer-Aided Design, 2023

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

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Threatpost Attack Stories 2021 (TAS21).

Megan K. Ryan, Kristin Yvonne Rozier

Dataset, March, 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

Satisfiability checking for Mission-time LTL (MLTL).

Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier

Inf. Comput., 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

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I.

Alexis A. Aurandt, Phillip H. Jones, Kristin Yvonne Rozier

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas.

Orion Staskal, Josh Simac, Logan Swayne, Kristin Y. Rozier

Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conferenc, 2022

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

Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

2021

Incremental design-space model checking via reusable reachable state approximations.

Rohit Dureja, Kristin Y. Rozier

Formal Methods Syst. Des., 2021

Towards a framework for certification of reliable autonomous systems.

Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Bernd-Holger Schlingloff, Michael Winikoff, Neil Yorke-Smith

Auton. Agents Multi Agent Syst., 2021

Integrating Runtime Verification into a Sounding Rocket Control System.

Benjamin Hertz, Zachary Luppen, Kristin Yvonne Rozier

Proceedings of the NASA Formal Methods - 13th International Symposium, 2021

Summarising a Framework for the Certification of Reliable Autonomous Systems.

Michael Fisher, Viviana Mascardi, Kristin Y. Rozier, Bernd-Holger Schlingloff, Michael Winikoff, Neil Yorke-Smith

Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

2020

Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks.

Rohit Dureja, Kristin Yvonne Rozier

J. Aerosp. Inf. Syst., July, 2020

SAT-based explicit LTLf satisfiability checking.

Jianwen Li, Geguang Pu, Yueling Zhang, Moshe Y. Vardi, Kristin Y. Rozier

Artif. Intell., 2020

Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2.

Brian Kempa, Pei Zhang, Phillip H. Jones, Joseph Zambreno, Kristin Yvonne Rozier

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration.

Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

Intersection and Rotation of Assumption Literals Boosts Bug-Finding.

Rohit Dureja, Jianwen Li, Geguang Pu, Moshe Y. Vardi, Kristin Y. Rozier

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2019

On Teaching Applied Formal Methods in Aerospace Engineering.

Kristin Yvonne Rozier

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques.

Kristin Yvonne Rozier

Proceedings of the 2019 Spring Simulation Conference, 2019

Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties.

Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, Kristin Y. Rozier

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Satisfiability Checking for Mission-Time LTL.

Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 ).

Rohit Dureja, Kristin Yvonne Rozier

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

MLTL Benchmark Generation via Formula Progression.

Jianwen Li, Kristin Y. Rozier

Proceedings of the Runtime Verification - 18th International Conference, 2018

A Broader View on Verification: From Static to Runtime and Back (Track Summary).

Wolfgang Ahrendt, Marieke Huisman, Giles Reger, Kristin Yvonne Rozier

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

SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability.

Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

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

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems.

Patrick Moosbrugger, Kristin Y. Rozier, Johann Schumann

Formal Methods Syst. Des., 2017

R2U2: Tool Overview.

Kristin Yvonne Rozier, Johann Schumann

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

On the Evaluation and Comparison of Runtime Verification Tools for Hardware and Cyber-Physical Systems.

Kristin Yvonne Rozier

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

FuseIC3: An algorithm for checking large design spaces.

Rohit Dureja, Kristin Yvonne Rozier

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

Specification: The Biggest Bottleneck in Formal Methods and Autonomy.

Kristin Yvonne Rozier

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2016

Runtime Analysis with R2U2: A Tool Exhibition Report.

Johann Schumann, Patrick Moosbrugger, Kristin Y. Rozier

Proceedings of the Runtime Verification - 16th International Conference, 2016

Cascading Solution to Data Dependence Constraints with Z3.

Eric William Davis Rozier, Kristin Y. Rozier

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2016

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.

Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Characterizing Data Dependence Constraints for Dynamic Reliability Using <i>N</i>-Queens Attack Domains.

Ulya Bayram, Kristin Yvonne Rozier, Eric William Davis Rozier

Proceedings of the Quantitative Evaluation of Systems, 12th International Conference, 2015

Comparing Different Functional Allocations in Automated Air Traffic Control Design.

Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, Kristin Y. Rozier

Proceedings of the Formal Methods in Computer-Aided Design, 2015

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

Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems.

Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Proceedings of the Runtime Verification - 5th International Conference, 2014

Probabilistic model checking for comparative analysis of automated air traffic control systems.

Yang Zhao, Kristin Y. Rozier

Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 2014

2012

Optimized temporal monitors for SystemC.

Deian Tabakov, Kristin Y. Rozier, Moshe Y. Vardi

Formal Methods Syst. Des., 2012

Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking.

Kristin Yvonne Rozier, Moshe Y. Vardi

Proceedings of the Hardware and Software: Verification and Testing, 2012

2011

Linear Temporal Logic Symbolic Model Checking.

Kristin Y. Rozier

Comput. Sci. Rev., 2011

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking.

Kristin Y. Rozier, Moshe Y. Vardi

Proceedings of the FM 2011: Formal Methods, 2011

2010

LTL satisfiability checking.

Kristin Y. Rozier, Moshe Y. Vardi

Int. J. Softw. Tools Technol. Transf., 2010