@techreport{NUREG-0899,
  title       = {Guidelines for the Preparation of Emergency Operating Procedures},
  author      = {{U.S. Nuclear Regulatory Commission}},
  institution = {U.S. Nuclear Regulatory Commission},
  year        = {1982},
  number      = {NUREG-0899}
}

@misc{10CFR50.34,
  title        = {{10 CFR Part 50.34}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {Code of Federal Regulations},
  urldate     = {2025-12-05},
  url          = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034}
}

@misc{10CFR55.59,
  title = {{10 CFR Part 55.59}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {Code of Federal Regulations},
  urldate     = {2025-12-05},
  url          = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059}
}

@techreport{WRPS.Description,
    title = {{Westinghouse RPS System Description}},
    institution = {Westinghouse Electric Corporation},
    url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf},
    urldate = {2025-12-05}
}

@online{gentillon_westinghouse_1999,
	title = {Westinghouse Reactor Protection System Unavailability, 1984-1995},
	url = {https://digital.library.unt.edu/ark:/67531/metadc620476/},
	titleaddon = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999},
	type = {Article},
	author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.},
	urldate = {2025-12-05},
	date = {1999-08-01},
	note = {Number: {INEEL}/{CON}-99-00374
Publisher: Idaho National Engineering and Environmental Laboratory},
	file = {Full Text PDF:/home/danesabo/Zotero/storage/7QKWQ8NI/Gentillon et al. - 1999 - Westinghouse Reactor Protection System Unavailability, 1984-1995.pdf:application/pdf},
}

@online{operator_statistics,
	title = {{Operator Licensing}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}},
	urldate = {2025-11-28},
	file = {Operator Licensing | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/KUP9B5GH/operator-licensing.html:text/html},
}

@misc{10CFR55,
	title = {{Part 55—Operators' Licenses}},
	author = {{U.S. Nuclear Regulatory Commission}},
	howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}},
}

@online{10CFR50.54,
	title = {{§ 50.54 Conditions of Licenses}},
  author = {{U.S. Nuclear Regulatory Commission}},
	howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}},
	urldate = {2025-11-28},
	file = {§ 50.54 Conditions of licenses. | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/THTZUD3T/part050-0054.html:text/html},
}

@techreport{Kemeny1979,
  title       = {Report of the President's Commission on the Accident at Three Mile Island},
  author      = {Kemeny, John G. and others},
  institution = {President's Commission on the Accident at Three Mile Island},
  year        = {1979},
  month       = {October}
}

@misc{WNA2020,
  title        = {Safety of Nuclear Power Reactors},
  author       = {{World Nuclear Association}},
  year         = {2020},
  howpublished = {\url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}}
}

@article{hogberg_root_2013,
	title = {Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants},
	volume = {42},
	issn = {0044-7447},
	url = {https://pmc.ncbi.nlm.nih.gov/articles/PMC3606704/},
	doi = {10.1007/s13280-013-0382-x},
	pages = {267--284},
	number = {3},
	journaltitle = {Ambio},
	shortjournal = {Ambio},
	author = {Högberg, Lars},
	urldate = {2025-12-05},
	date = {2013-04},
	pmid = {23423737},
	pmcid = {PMC3606704},
	file = {Full Text:/home/danesabo/Zotero/storage/E8F2QZGR/Högberg - 2013 - Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants.pdf:application/pdf},
}

@article{zhang_analysis_2025,
	title = {Analysis of human errors in nuclear power plant event reports},
	volume = {57},
	issn = {1738-5733},
	url = {https://www.sciencedirect.com/science/article/pii/S1738573325002554},
	doi = {10.1016/j.net.2025.103687},
	pages = {103687},
	number = {10},
	journaltitle = {Nuclear Engineering and Technology},
	shortjournal = {Nuclear Engineering and Technology},
	author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng},
	urldate = {2025-12-05},
	date = {2025-10-01},
	keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports},
	file = {ScienceDirect Snapshot:/home/danesabo/Zotero/storage/N5R2Z3GL/S1738573325002554.html:text/html},
}

@techreport{Kiniry2024,
  title       = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report},
  author      = {Kiniry, Joseph and Bakst, Alexander and Hansen, Simon and Podhradsky, Michal and Bivin, Andrew},
  institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission},
  year        = {2024},
  number      = {TLR-RES-RES/DE-2024-005},
  note        = {NRC Contract 31310021C0014}
}

@techreport{eia_lcoe_2022,
  author       = {{U.S. Energy Information Administration}},
  title        = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022},
  institution  = {U.S. Energy Information Administration},
  year         = {2022},
  month        = {March},
  type         = {Report},
  url          = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf},
  note         = {See Table 1b, page 9}
}

@misc{eesi_datacenter_2024,
  author       = {{Environmental and Energy Study Institute}},
  title        = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate},
  howpublished = {Web article},
  year         = {2024},
  url          = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate},
  note         = {Accessed: 2025-09-29}
}

@book{baier_principles_2008,
	location = {Cambridge, {MA}, {USA}},
	title = {Principles of Model Checking},
	isbn = {978-0-262-02649-9},
	abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
	pagetotal = {984},
	publisher = {{MIT} Press},
	author = {Baier, Christel and Katoen, Joost-Pieter},
	date = {2008-04-25},
	langid = {english},
}

@inproceedings{katis_capture_2022,
	location = {Cham},
	title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}},
	isbn = {978-3-031-13188-2},
	doi = {10.1007/978-3-031-13188-2_24},
	shorttitle = {Capture, Analyze, Diagnose},
	pages = {490--504},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
	editor = {Shoham, Sharon and Vizel, Yakir},
	date = {2022},
	langid = {english},
	file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf},
}

@inproceedings{meyer_strix_2018,
	location = {Cham},
	title = {Strix: Explicit Reactive Synthesis Strikes Back!},
	isbn = {978-3-319-96145-3},
	doi = {10.1007/978-3-319-96145-3_31},
	shorttitle = {Strix},
	pages = {578--586},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael},
	editor = {Chockler, Hana and Weissenbacher, Georg},
	date = {2018},
	langid = {english},
}

@misc{jacobs_reactive_2024,
	title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021},
	url = {http://arxiv.org/abs/2206.00251},
	doi = {10.48550/arXiv.2206.00251},
	shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})},
	number = {{arXiv}:2206.00251},
	publisher = {{arXiv}},
	author = {Jacobs, Swen and others},
	urldate = {2025-12-06},
	date = {2024-05-06},
	eprinttype = {arxiv},
	eprint = {2206.00251 [cs]},
	keywords = {Computer Science - Logic in Computer Science},
	file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html},
}

@article{branicky_multiple_1998,
	title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
	volume = {43},
	issn = {1558-2523},
	url = {https://ieeexplore.ieee.org/document/664150},
	doi = {10.1109/9.664150},
	pages = {475--482},
	number = {4},
	journaltitle = {{IEEE} Transactions on Automatic Control},
	author = {Branicky, M.S.},
	urldate = {2025-09-10},
	date = {1998-04},
	keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches},
	file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf},
}

@thesis{guernic_reachability_2009,
	title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics},
	url = {https://theses.hal.science/tel-00422569},
	institution = {Université Joseph-Fourier - Grenoble I},
	type = {phdthesis},
	author = {Guernic, Colas Le},
	urldate = {2025-09-14},
	date = {2009-10-28},
	langid = {english},
	file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf},
}

@inproceedings{alur_hybrid_1993,
	location = {Berlin, Heidelberg},
	title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
	isbn = {978-3-540-48060-0},
	doi = {10.1007/3-540-57318-6_30},
	shorttitle = {Hybrid automata},
	pages = {209--229},
	booktitle = {Hybrid Systems},
	publisher = {Springer},
	author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
	editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
	date = {1993},
	langid = {english},
	keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
	file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf},
}

@article{mitchell_time-dependent_2005,
	title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
	volume = {50},
	issn = {1558-2523},
	url = {https://ieeexplore.ieee.org/abstract/document/1463302},
	doi = {10.1109/TAC.2005.851439},
	pages = {947--957},
	number = {7},
	journaltitle = {{IEEE} Transactions on Automatic Control},
	author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.},
	urldate = {2025-09-15},
	date = {2005-07},
	keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity},
	file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf},
}

@inproceedings{frehse_spaceex_2011,
	location = {Berlin, Heidelberg},
	title = {{SpaceEx}: Scalable Verification of Hybrid Systems},
	isbn = {978-3-642-22110-1},
	doi = {10.1007/978-3-642-22110-1_30},
	shorttitle = {{SpaceEx}},
	pages = {379--395},
	booktitle = {Computer Aided Verification},
	publisher = {Springer},
	author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
	editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
	date = {2011},
	langid = {english},
	keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function},
	file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf},
}

@inproceedings{bansal_hamilton-jacobi_2017,
	title = {Hamilton-Jacobi reachability: A brief overview and recent advances},
	url = {https://ieeexplore.ieee.org/abstract/document/8263977},
	doi = {10.1109/CDC.2017.8263977},
	shorttitle = {Hamilton-Jacobi reachability},
	eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
	pages = {2242--2253},
	booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
	author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
	urldate = {2025-09-15},
	date = {2017-12},
	keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials},
	file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf},
}

@inproceedings{prajna_safety_2004,
	location = {Berlin, Heidelberg},
	title = {Safety Verification of Hybrid Systems Using Barrier Certificates},
	isbn = {978-3-540-24743-2},
	doi = {10.1007/978-3-540-24743-2_32},
	pages = {477--492},
	booktitle = {Hybrid Systems: Computation and Control},
	publisher = {Springer},
	author = {Prajna, Stephen and Jadbabaie, Ali},
	editor = {Alur, Rajeev and Pappas, George J.},
	date = {2004},
	langid = {english},
	keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis},
}