default search action
Kristin Y. Rozier
Person information
- affiliation: Iowa State University, USA
- affiliation (former): NASA, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2025
- [e6]André Platzer
, Kristin Yvonne Rozier
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14933, Springer 2025, ISBN 978-3-031-71161-9 [contents] - [e5]André Platzer
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14934, Springer 2025, ISBN 978-3-031-71176-3 [contents] - 2024
- [c48]Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier:
The MoXI Model Exchange Tool Suite. CAV (1) 2024: 203-218 - [c47]Alexis A. Aurandt
Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems. FMICS 2024: 220-244 - [c46]Katherine Kosaian
Formalizing Coppersmith's Method in Isabelle/HOL. CICM 2024: 127-145 - [c45]Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi:
MoXI: An Intermediate Language for Symbolic Model Checking. SPIN 2024: 26-46 - [c44]Kristin Yvonne Rozier
R2U2: Runtime Verification Takes Off! (Keynote). VORTEX@ISSTA 2024: 1 - [i4]Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Y. Rozier:
Formalizing MLTL Formula Progression in Isabelle/HOL. CoRR abs/2410.03465 (2024) - 2023
- [c43]Chris Johannsen, Phillip H. Jones, Brian Kempa, Kristin Yvonne Rozier, Pei Zhang:
R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software. CAV (3) 2023: 483-497 - [c42]Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi:
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. FMCAD 2023: 1 - [c41]Chris Johannsen, Brian Kempa, Phillip H. Jones, Kristin Y. Rozier, Tichakorn Wongpiromsarn:
Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints. FMICS 2023: 151-169 - [c40]Gokul Hariharan
Maximum Satisfiability of Mission-Time Linear Temporal Logic. FORMATS 2023: 86-104 - [c39]Pei Zhang
Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines. FORMATS 2023: 158-180 - [c38]Jenna Elwing, Laura Gamboa-Guzman
Mission-Time LTL (MLTL) Formula Validation via Regular Expressions. iFM 2023: 279-301 - [c37]Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier:
What's in a Name? Linear Temporal Logic Literally Represents Time Lines. VISSOFT 2023: 73-83 - [c36]Laura P. Gamboa Guzman, Kristin Y. Rozier:
Stalnaker's Epistemic Logic in Isabelle/HOL. LSFA/HCVS 2023: 4-17 - [e4]Alexander Nadel, Kristin Yvonne Rozier:
Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023. IEEE 2023, ISBN 978-3-85448-060-0 [contents] - [e3]Kristin Yvonne Rozier
NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings. Lecture Notes in Computer Science 13903, Springer 2023, ISBN 978-3-031-33169-5 [contents] - [i3]Ellen Enkel, Nils Jansen, Mohammad Reza Mousavi, Kristin Yvonne Rozier:
Model Learning for Improved Trustworthiness in Autonomous Systems (Dagstuhl Seminar 23492). Dagstuhl Reports 13(12): 24-47 (2023) - 2022
- [j13]Jianwen Li
Satisfiability checking for Mission-time LTL (MLTL). Inf. Comput. 289(Part): 104923 (2022) - [j12]Abigail Hammer
Integrating runtime verification into an automated UAS traffic management system. Innov. Syst. Softw. Eng. 18(4): 567-580 (2022) - [c35]Gokul Hariharan
MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types. NSV/FoMLAS@CAV 2022: 187-204 - [c34]Orion Staskal, Josh Simac, Logan Swayne, Kristin Y. Rozier:
Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas. COMPSAC 2022: 1637-1642 - [c33]Zachary Luppen
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry. NFM 2022: 527-537 - [c32]Alexis A. Aurandt
Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I. NFM 2022: 816-825 - [d1]Megan K. Ryan
Threatpost Attack Stories 2021 (TAS21). IEEE DataPort, 2022 - 2021
- [j11]Michael Fisher
Towards a framework for certification of reliable autonomous systems. Auton. Agents Multi Agent Syst. 35(1): 8 (2021) - [j10]Rohit Dureja
Incremental design-space model checking via reusable reachable state approximations. Formal Methods Syst. Des. 58(3): 375-398 (2021) - [c31]Michael Fisher, Viviana Mascardi, Kristin Y. Rozier, Bernd-Holger Schlingloff, Michael Winikoff, Neil Yorke-Smith:
Summarising a Framework for the Certification of Reliable Autonomous Systems. AAMAS 2021: 1733-1734 - [c30]Benjamin Hertz
Integrating Runtime Verification into a Sounding Rocket Control System. NFM 2021: 151-159 - 2020
- [j9]Jianwen Li, Geguang Pu, Yueling Zhang, Moshe Y. Vardi
SAT-based explicit LTLf satisfiability checking. Artif. Intell. 289: 103369 (2020) - [j8]Rohit Dureja
Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks. J. Aerosp. Inf. Syst. 17(7): 322-335 (2020) - [c29]Matthew Cauwels
Integrating Runtime Verification into an Automated UAS Traffic Management System. ECSA Companion 2020: 340-357 - [c28]Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier:
Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. FMCAD 2020: 16-25 - [c27]Brian Kempa
Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. FORMATS 2020: 196-214 - [i2]Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Bernd-Holger Schlingloff, Michael Winikoff, Neil Yorke-Smith:
Towards a Framework for Certification of Reliable Autonomous Systems. CoRR abs/2001.09124 (2020)
2010 – 2019
- 2019
- [c26]Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi:
SAT-Based Explicit LTLf Satisfiability Checking. AAAI 2019: 2946-2953 - [c25]Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier:
Satisfiability Checking for Mission-Time LTL. CAV (2) 2019: 3-22 - [c24]Rohit Dureja
Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties. FMCAD 2019: 1-9 - [c23]Kristin Yvonne Rozier:
From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques. SpringSim 2019: 1-10 - [c22]Kristin Yvonne Rozier
On Teaching Applied Formal Methods in Aerospace Engineering. FMTea 2019: 111-131 - [c21]Rohit Dureja, Jianwen Li, Geguang Pu, Moshe Y. Vardi, Kristin Y. Rozier:
Intersection and Rotation of Assumption Literals Boosts Bug-Finding. VSTTE 2019: 180-192 - [e2]Julia M. Badger, Kristin Yvonne Rozier:
NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings. Lecture Notes in Computer Science 11460, Springer 2019, ISBN 978-3-030-20651-2 [contents] - 2018
- [c20]Jianwen Li, Rohit Dureja
SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. CAV (2) 2018: 37-44 - [c19]Wolfgang Ahrendt, Marieke Huisman
A Broader View on Verification: From Static to Runtime and Back (Track Summary). ISoLA (2) 2018: 3-7 - [c18]Jianwen Li, Kristin Y. Rozier:
MLTL Benchmark Generation via Formula Progression. RV 2018: 426-433 - [c17]Rohit Dureja
More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 ). TACAS (1) 2018: 309-327 - [i1]Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi:
SAT-based Explicit LTLf Satisfiability Checking. CoRR abs/1811.03176 (2018) - 2017
- [j7]Patrick Moosbrugger, Kristin Y. Rozier, Johann Schumann:
R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods Syst. Des. 51(1): 31-61 (2017) - [j6]Eric William Davis Rozier, Kristin Y. Rozier, Ulya Bayram
Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains. Leibniz Trans. Embed. Syst. 4(1): 05:1-05:26 (2017) - [c16]Rohit Dureja
FuseIC3: An algorithm for checking large design spaces. FMCAD 2017: 164-171 - [c15]Kristin Yvonne Rozier:
On the Evaluation and Comparison of Runtime Verification Tools for Hardware and Cyber-Physical Systems. RV-CuBES 2017: 123-137 - [c14]Kristin Yvonne Rozier, Johann Schumann:
R2U2: Tool Overview. RV-CuBES 2017: 138-156 - 2016
- [c13]Marco Gario
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. CAV (2) 2016: 3-22 - [c12]Eric William Davis Rozier, Kristin Y. Rozier:
Cascading Solution to Data Dependence Constraints with Z3. ISAIM 2016 - [c11]Johann Schumann, Patrick Moosbrugger, Kristin Y. Rozier:
Runtime Analysis with R2U2: A Tool Exhibition Report. RV 2016: 504-509 - [c10]Kristin Yvonne Rozier:
Specification: The Biggest Bottleneck in Formal Methods and Autonomy. VSTTE 2016: 8-26 - 2015
- [c9]Cristian Mattarei, Alessandro Cimatti
Comparing Different Functional Allocations in Automated Air Traffic Control Design. FMCAD 2015: 112-119 - [c8]Ulya Bayram
Characterizing Data Dependence Constraints for Dynamic Reliability Using N-Queens Attack Domains. QEST 2015: 211-227 - [c7]Johann Schumann, Patrick Moosbrugger, Kristin Y. Rozier:
R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems. RV 2015: 233-249 - 2014
- [j5]Yang Zhao, Kristin Yvonne Rozier:
Formal specification and verification of a coordination protocol for an automated air traffic control system. Sci. Comput. Program. 96: 337-353 (2014) - [c6]Yang Zhao, Kristin Y. Rozier:
Probabilistic model checking for comparative analysis of automated air traffic control systems. ICCAD 2014: 690-695 - [c5]Johannes Geist, Kristin Y. Rozier, Johann Schumann:
Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems. RV 2014: 215-230 - [c4]Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann:
Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems. TACAS 2014: 357-372 - [e1]Julia M. Badger, Kristin Yvonne Rozier:
NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings. Lecture Notes in Computer Science 8430, Springer 2014, ISBN 978-3-319-06199-3 [contents] - 2012
- [j4]Yang Zhao, Kristin Yvonne Rozier:
Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012) - [j3]Deian Tabakov, Kristin Y. Rozier, Moshe Y. Vardi:
Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41(3): 236-268 (2012) - [c3]Kristin Yvonne Rozier, Moshe Y. Vardi:
Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking. Haifa Verification Conference 2012: 243-259 - 2011
- [j2]Kristin Y. Rozier:
Linear Temporal Logic Symbolic Model Checking. Comput. Sci. Rev. 5(2): 163-203 (2011) - [c2]Kristin Y. Rozier, Moshe Y. Vardi:
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. FM 2011: 417-431 - 2010
- [j1]Kristin Y. Rozier, Moshe Y. Vardi:
LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12(2): 123-137 (2010)
2000 – 2009
- 2007
- [c1]Kristin Y. Rozier, Moshe Y. Vardi:
LTL Satisfiability Checking. SPIN 2007: 149-167
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 21:45 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: