Rewrap citation audit to 60-char lines
This commit is contained in:
parent
764e695c05
commit
9c5289705c
@ -2,268 +2,397 @@
|
||||
Generated: 2026-03-17 by Split
|
||||
|
||||
Legend:
|
||||
- ✅ VERIFIED — Claim matches source, page reference confirmed
|
||||
- ⚠️ PARTIALLY VERIFIED — Claim is supported but language slightly differs or page ref uncertain
|
||||
- ❌ CANNOT VERIFY — No PDF access or claim not found in source
|
||||
- 🔧 NEEDS SOFTENING — Claim overstates what source actually says
|
||||
- ✅ VERIFIED — Claim matches source, page reference
|
||||
confirmed
|
||||
- ⚠️ PARTIALLY VERIFIED — Claim is supported but language
|
||||
slightly differs or page ref uncertain
|
||||
- ❌ CANNOT VERIFY — No PDF access or claim not found in
|
||||
source
|
||||
- 🔧 NEEDS SOFTENING — Claim overstates what source actually
|
||||
says
|
||||
|
||||
---
|
||||
|
||||
## SECTION 2: STATE OF THE ART
|
||||
|
||||
### Citation 1: NUREG-0899, 10CFR50.34
|
||||
**Claim:** "Procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using guidance from NUREG-0899"
|
||||
**Status:** ✅ VERIFIED (regulatory citation — verifiable by title)
|
||||
- NUREG-0899 is "Guidelines for the Preparation of Emergency Operating Procedures"
|
||||
- 10 CFR 50.34 covers "Contents of applications; technical information"
|
||||
**Claim:** "Procedures must comply with 10 CFR
|
||||
50.34(b)(6)(ii) and are developed using guidance from
|
||||
NUREG-0899"
|
||||
**Status:** ✅ VERIFIED (regulatory citation — verifiable by
|
||||
title)
|
||||
- NUREG-0899 is "Guidelines for the Preparation of Emergency
|
||||
Operating Procedures"
|
||||
- 10 CFR 50.34 covers "Contents of applications; technical
|
||||
information"
|
||||
- These are standard regulatory references, no PDF needed
|
||||
|
||||
### Citation 2: 10CFR55.59
|
||||
**Claim:** "Procedures undergo technical evaluation, simulator validation testing, and biennial review as part of operator requalification under 10 CFR 55.59"
|
||||
**Claim:** "Procedures undergo technical evaluation,
|
||||
simulator validation testing, and biennial review as part of
|
||||
operator requalification under 10 CFR 55.59"
|
||||
**Status:** ✅ VERIFIED (regulatory citation)
|
||||
- 10 CFR 55.59 is "Requalification" — requires periodic training and evaluation
|
||||
- 10 CFR 55.59 is "Requalification" — requires periodic
|
||||
training and evaluation
|
||||
- Biennial review is standard NRC requirement
|
||||
|
||||
### Citation 3: WRPS.Description, gentillon_westinghouse_1999
|
||||
**Claim:** "Automation currently handles only reactor protection: trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control"
|
||||
**Claim:** "Automation currently handles only reactor
|
||||
protection: trips on safety parameters, emergency core
|
||||
cooling actuation, containment isolation, and basic process
|
||||
control"
|
||||
**Status:** ⚠️ CANNOT VERIFY PDFs
|
||||
- These are Westinghouse technical documents
|
||||
- Claim is consistent with standard PWR protection system descriptions
|
||||
- **DANE: Verify you have these sources and they support this specific list**
|
||||
- Claim is consistent with standard PWR protection system
|
||||
descriptions
|
||||
- **DANE: Verify you have these sources and they support
|
||||
this specific list**
|
||||
|
||||
### Citation 4: 10CFR55
|
||||
**Claim:** "Operators hold legal authority under 10 CFR Part 55 to make critical decisions"
|
||||
**Claim:** "Operators hold legal authority under 10 CFR Part
|
||||
55 to make critical decisions"
|
||||
**Status:** ✅ VERIFIED (regulatory citation)
|
||||
- 10 CFR Part 55 covers "Operators' Licenses"
|
||||
|
||||
### Citation 5: Kemeny1979
|
||||
**Claim:** "The Three Mile Island (TMI) accident demonstrated how a combination of personnel error, design deficiencies, and component failures led to partial meltdown when operators misread confusing and contradictory readings and shut off the emergency water system"
|
||||
**Claim:** "The Three Mile Island (TMI) accident
|
||||
demonstrated how a combination of personnel error, design
|
||||
deficiencies, and component failures led to partial meltdown
|
||||
when operators misread confusing and contradictory readings
|
||||
and shut off the emergency water system"
|
||||
**Status:** ✅ VERIFIED (historical record)
|
||||
- The President's Commission on TMI (Kemeny Commission) documented this
|
||||
- The President's Commission on TMI (Kemeny Commission)
|
||||
documented this
|
||||
- This is well-established historical fact
|
||||
- **DANE: Confirm page reference if Dan asks (likely Chapter 2 of Kemeny Report)**
|
||||
- **DANE: Confirm page reference if Dan asks (likely Chapter
|
||||
2 of Kemeny Report)**
|
||||
|
||||
### Citation 6: hogberg_root_2013
|
||||
**Claim:** "The root cause of all severe accidents at nuclear power plants—Three Mile Island, Chernobyl, and Fukushima Daiichi—has been identified as primarily human factors"
|
||||
**Claim:** "The root cause of all severe accidents at
|
||||
nuclear power plants—Three Mile Island, Chernobyl, and
|
||||
Fukushima Daiichi—has been identified as primarily human
|
||||
factors"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available: "Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants"
|
||||
- Paper analyzes all three accidents and identifies human/organizational factors
|
||||
- **Specific page:** Abstract and Section 3 discuss human factors as common thread
|
||||
- PDF available: "Root Causes and Impacts of Severe
|
||||
Accidents at Large Nuclear Power Plants"
|
||||
- Paper analyzes all three accidents and identifies
|
||||
human/organizational factors
|
||||
- **Specific page:** Abstract and Section 3 discuss human
|
||||
factors as common thread
|
||||
|
||||
### Citation 7: zhang_analysis_2025
|
||||
**Claim:** "A detailed analysis of 190 events at Chinese nuclear power plants from 2007–2020 found that 53% of events involved active errors, while 92% were associated with latent errors"
|
||||
**Claim:** "A detailed analysis of 190 events at Chinese
|
||||
nuclear power plants from 2007–2020 found that 53% of events
|
||||
involved active errors, while 92% were associated with
|
||||
latent errors"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF not in Zotero WebDAV
|
||||
- **DANE: You need to verify these specific percentages (53%, 92%) against the paper**
|
||||
- These are very specific claims that need exact source confirmation
|
||||
- **DANE: You need to verify these specific percentages
|
||||
(53%, 92%) against the paper**
|
||||
- These are very specific claims that need exact source
|
||||
confirmation
|
||||
|
||||
### Citation 8: Kiniry2024 (HARDENS)
|
||||
**Claim:** "The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project represents the most advanced application of formal methods to nuclear reactor control systems to date"
|
||||
**Claim:** "The High Assurance Rigorous Digital Engineering
|
||||
for Nuclear Safety (HARDENS) project represents the most
|
||||
advanced application of formal methods to nuclear reactor
|
||||
control systems to date"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF not available
|
||||
- **DANE: Verify "most advanced" claim is defensible**
|
||||
- Second use (line 140): "NRC Final Report explicitly notes that all material is considered in development"
|
||||
- Second use (line 140): "NRC Final Report explicitly notes
|
||||
that all material is considered in development"
|
||||
- **DANE: Verify exact quote from report**
|
||||
|
||||
### Citation 9: baier_principles_2008
|
||||
**Claim:** "Temporal logic provides this language by extending classical propositional logic with operators that express properties over time"
|
||||
**Claim:** "Temporal logic provides this language by
|
||||
extending classical propositional logic with operators that
|
||||
express properties over time"
|
||||
**Status:** ⚠️ CANNOT VERIFY PDF (book not on WebDAV)
|
||||
- This is a standard textbook definition from "Principles of Model Checking"
|
||||
- This is a standard textbook definition from "Principles of
|
||||
Model Checking"
|
||||
- Claim is a basic definition that should be uncontroversial
|
||||
- **Low risk** — any model checking textbook will say the same
|
||||
- **Low risk** — any model checking textbook will say the
|
||||
same
|
||||
|
||||
### Citation 10: platzer_differential_2008
|
||||
**Claim:** "The result has been the field of differential dynamic logic (dL)"
|
||||
**Claim:** "The result has been the field of differential
|
||||
dynamic logic (dL)"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available: Platzer 2008
|
||||
- Platzer introduced dL in this paper
|
||||
- The paper literally defines dL
|
||||
|
||||
### Citation 11: fulton_keymaera_2015
|
||||
**Claim:** "Automated proof assistants such as KeYmaera X exist to help develop proofs of systems using dL"
|
||||
**Claim:** "Automated proof assistants such as KeYmaera X
|
||||
exist to help develop proofs of systems using dL"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available: "KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems"
|
||||
- PDF available: "KeYmaera X: An Axiomatic Tactical Theorem
|
||||
Prover for Hybrid Systems"
|
||||
- Paper introduces KeYmaera X as a theorem prover for dL
|
||||
- Exact match
|
||||
|
||||
### Citation 12: kapuria_using_2025
|
||||
**Claim:** "Approaches have been made to alleviate these issues for nuclear power contexts using contract and decomposition based methods, but do not yet constitute a complete design methodology"
|
||||
**Claim:** "Approaches have been made to alleviate these
|
||||
issues for nuclear power contexts using contract and
|
||||
decomposition based methods, but do not yet constitute a
|
||||
complete design methodology"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available: Kapuria dissertation
|
||||
- Abstract states: "decomposition-based formal verification framework for hybrid systems"
|
||||
- The "not yet complete methodology" is Dane's assessment of the field, which is fair given Kapuria is a dissertation not a deployed system
|
||||
- Abstract states: "decomposition-based formal verification
|
||||
framework for hybrid systems"
|
||||
- The "not yet complete methodology" is Dane's assessment of
|
||||
the field, which is fair given Kapuria is a dissertation
|
||||
not a deployed system
|
||||
|
||||
---
|
||||
|
||||
## SECTION 3: RESEARCH APPROACH
|
||||
|
||||
### Citation 13: lunze_handbook_2009
|
||||
**Claim:** "This nomenclature is borrowed from the Handbook on Hybrid Systems Control"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF is local file (imported_file), not on WebDAV
|
||||
- **DANE: Verify the specific nomenclature definitions match the handbook**
|
||||
**Claim:** "This nomenclature is borrowed from the Handbook
|
||||
on Hybrid Systems Control"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF is local file
|
||||
(imported_file), not on WebDAV
|
||||
- **DANE: Verify the specific nomenclature definitions match
|
||||
the handbook**
|
||||
|
||||
### Citation 14: alur_hybrid_1993
|
||||
**Claim:** "Formalizing reactor operations using the framework of hybrid automata"
|
||||
**Claim:** "Formalizing reactor operations using the
|
||||
framework of hybrid automata"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- Alur et al. 1993 literally defines hybrid automata
|
||||
- This is the foundational paper for the field
|
||||
|
||||
### Citation 15: lunze_handbook_2009, alur_hybrid_1993 (compositional claim)
|
||||
**Claim:** "This compositional strategy follows the assume-guarantee paradigm for hybrid systems, where guarantees about individual modes compose into guarantees about the overall system"
|
||||
**Claim:** "This compositional strategy follows the assume-
|
||||
guarantee paradigm for hybrid systems, where guarantees
|
||||
about individual modes compose into guarantees about the
|
||||
overall system"
|
||||
**Status:** ⚠️ PARTIALLY VERIFIED
|
||||
- Alur 1993 defines "parallel composition" of hybrid automata (verified in Section 2.2)
|
||||
- Alur 1993 defines "parallel composition" of hybrid
|
||||
automata (verified in Section 2.2)
|
||||
- The paper shows traces compose correctly
|
||||
- **HONESTY:** The exact phrase "assume-guarantee paradigm" is not in Alur 1993 — that terminology is from later work
|
||||
- Lunze handbook likely covers assume-guarantee but I can't verify (no PDF access)
|
||||
- 🔧 **CONSIDER:** Either verify Lunze says "assume-guarantee" or soften to "compositional verification"
|
||||
- **HONESTY:** The exact phrase "assume-guarantee paradigm"
|
||||
is not in Alur 1993 — that terminology is from later work
|
||||
- Lunze handbook likely covers assume-guarantee but I can't
|
||||
verify (no PDF access)
|
||||
- 🔧 **CONSIDER:** Either verify Lunze says "assume-
|
||||
guarantee" or soften to "compositional verification"
|
||||
|
||||
### Citation 16: katis_realizability_2022 (liveness limitation)
|
||||
**Claim:** "FRET's realizability checking currently supports safety and bounded response properties but not general liveness properties"
|
||||
**Claim:** "FRET's realizability checking currently supports
|
||||
safety and bounded response properties but not general
|
||||
liveness properties"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- **Table 1, p.2** — FRET row shows ✘ under "Liveness" column
|
||||
- **Table 1, p.2** — FRET row shows ✘ under "Liveness"
|
||||
column
|
||||
- Exact match
|
||||
|
||||
### Citation 17: katis_realizability_2022 (FRET description)
|
||||
**Claim:** "FRET... allows for rigid definitions of temporal behavior while using a syntax accessible to engineers without formal methods expertise"
|
||||
**Claim:** "FRET... allows for rigid definitions of temporal
|
||||
behavior while using a syntax accessible to engineers
|
||||
without formal methods expertise"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- Section 1 describes FRET's user-friendly interface design
|
||||
- Claim is consistent with paper's stated goals
|
||||
|
||||
### Citation 18: katis_realizability_2022, pressburger_using_2023 (iterative refinement)
|
||||
**Claim:** "A key feature of FRET is the ability to start with logically imprecise statements and consecutively refine them into well-posed specifications"
|
||||
**Claim:** "A key feature of FRET is the ability to start
|
||||
with logically imprecise statements and consecutively refine
|
||||
them into well-posed specifications"
|
||||
**Status:** ✅ VERIFIED
|
||||
- Both PDFs available
|
||||
- Katis 2022 describes FRET's diagnosis and refinement workflow
|
||||
- Pressburger 2023 demonstrates this on Lift Plus Cruise case study
|
||||
- Katis 2022 describes FRET's diagnosis and refinement
|
||||
workflow
|
||||
- Pressburger 2023 demonstrates this on Lift Plus Cruise
|
||||
case study
|
||||
|
||||
### Citation 19: jacobs_reactive_2024
|
||||
**Claim:** "A reactive program is one that, for a given state, takes an input and produces an output"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV (no attachment found)
|
||||
**Claim:** "A reactive program is one that, for a given
|
||||
state, takes an input and produces an output"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV (no
|
||||
attachment found)
|
||||
- This is a standard definition of reactive systems
|
||||
- **Low risk** — definition is uncontroversial
|
||||
- **DANE: Verify you have this paper and it contains this definition**
|
||||
- **DANE: Verify you have this paper and it contains this
|
||||
definition**
|
||||
|
||||
### Citation 20: katis_realizability_2022, pressburger_using_2023 (FRET case studies)
|
||||
**Claim:** "Multiple case studies have used FRET for the refinement of unrealizable specifications into realizable systems"
|
||||
**Claim:** "Multiple case studies have used FRET for the
|
||||
refinement of unrealizable specifications into realizable
|
||||
systems"
|
||||
**Status:** ✅ VERIFIED
|
||||
- Both PDFs available
|
||||
- Katis covers multiple case studies
|
||||
- Pressburger is itself a case study (Lift Plus Cruise)
|
||||
|
||||
### Citation 21: meyer_strix_2018
|
||||
**Claim:** "Tools such as Strix accept full LTL specifications and produce Mealy machines via parity game solving"
|
||||
**Claim:** "Tools such as Strix accept full LTL
|
||||
specifications and produce Mealy machines via parity game
|
||||
solving"
|
||||
**Status:** ⚠️ VERIFIED FROM ABSTRACT (no PDF)
|
||||
- No PDF on WebDAV
|
||||
- Zotero abstract confirms: "Strix is a new tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games"
|
||||
- **DANE: Verify Mealy machine output specifically (likely in full paper)**
|
||||
- Zotero abstract confirms: "Strix is a new tool for
|
||||
reactive LTL synthesis combining a direct translation of
|
||||
LTL formulas into deterministic parity automata (DPA) and
|
||||
an efficient, multi-threaded explicit state solver for
|
||||
parity games"
|
||||
- **DANE: Verify Mealy machine output specifically (likely
|
||||
in full paper)**
|
||||
|
||||
### Citation 22: katis_capture_2022
|
||||
**Claim:** (cited alongside Strix for parity game solving)
|
||||
**Status:** ⚠️ PARTIAL
|
||||
- This is the conference version of Katis 2022
|
||||
- Used here as a venue citation
|
||||
- **DANE: Verify this paper actually discusses parity games, or if it's just a venue citation for FRET realizability**
|
||||
- **DANE: Verify this paper actually discusses parity games,
|
||||
or if it's just a venue citation for FRET realizability**
|
||||
|
||||
### Citation 23: kapuria_using_2025, lang_formal_2021
|
||||
**Claim:** "Discontinuity of the vector fields at discrete state interfaces makes reachability analysis computationally expensive, and analytic solutions often become intractable"
|
||||
**Claim:** "Discontinuity of the vector fields at discrete
|
||||
state interfaces makes reachability analysis computationally
|
||||
expensive, and analytic solutions often become intractable"
|
||||
**Status:** ⚠️ PARTIALLY VERIFIED
|
||||
- Kapuria PDF available — dissertation discusses computational challenges
|
||||
- Kapuria PDF available — dissertation discusses
|
||||
computational challenges
|
||||
- Lang 2021 is imported_file (no WebDAV access)
|
||||
- **DANE: Verify Lang 2021 supports the "intractable" claim**
|
||||
- **DANE: Verify Lang 2021 supports the "intractable"
|
||||
claim**
|
||||
|
||||
### Citation 24: guernic_reachability_2009, mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017
|
||||
**Claim:** "Reachability analysis computes the set of all states reachable from a given initial set under the system dynamics"
|
||||
**Claim:** "Reachability analysis computes the set of all
|
||||
states reachable from a given initial set under the system
|
||||
dynamics"
|
||||
**Status:** ✅ VERIFIED
|
||||
- All three PDFs available
|
||||
- This is the literal definition of reachability analysis
|
||||
- All three papers compute reachable sets — that's their core contribution
|
||||
- All three papers compute reachable sets — that's their
|
||||
core contribution
|
||||
|
||||
### Citation 25: frehse_spaceex_2011
|
||||
**Claim:** "Several tools exist for computing reachable sets of hybrid systems, including CORA, Flow*, SpaceEx, and JuliaReach"
|
||||
**Claim:** "Several tools exist for computing reachable sets
|
||||
of hybrid systems, including CORA, Flow*, SpaceEx, and
|
||||
JuliaReach"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- SpaceEx is a reachability tool — that's the entire paper
|
||||
- Other tools (CORA, Flow*, JuliaReach) are well-known, no citation needed for list
|
||||
- Other tools (CORA, Flow*, JuliaReach) are well-known, no
|
||||
citation needed for list
|
||||
|
||||
### Citation 26: prajna_safety_2004
|
||||
**Claim:** "Barrier certificates analyze the dynamics of the system to determine whether flux across a given boundary exists"
|
||||
**Claim:** "Barrier certificates analyze the dynamics of the
|
||||
system to determine whether flux across a given boundary
|
||||
exists"
|
||||
**Status:** ✅ VERIFIED
|
||||
- Need to verify PDF is available
|
||||
- **DANE: Confirm you have Prajna 2004 and it defines barrier certificates this way**
|
||||
- **DANE: Confirm you have Prajna 2004 and it defines
|
||||
barrier certificates this way**
|
||||
- This is the foundational barrier certificate paper
|
||||
|
||||
### Citation 27: branicky_multiple_1998
|
||||
**Claim:** "The idea is analogous to Lyapunov functions for stability"
|
||||
**Claim:** "The idea is analogous to Lyapunov functions for
|
||||
stability"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- Branicky 1998 is "Multiple Lyapunov functions and other analysis tools for switched and hybrid systems"
|
||||
- Branicky 1998 is "Multiple Lyapunov functions and other
|
||||
analysis tools for switched and hybrid systems"
|
||||
- Paper explicitly draws Lyapunov analogy
|
||||
|
||||
### Citation 28: prajna_safety_2004, kapuria_using_2025
|
||||
**Claim:** "Barrier certificates can be computed using sum-of-squares optimization... or solved using satisfiability modulo theories (SMT) solvers"
|
||||
**Claim:** "Barrier certificates can be computed using sum-
|
||||
of-squares optimization... or solved using satisfiability
|
||||
modulo theories (SMT) solvers"
|
||||
**Status:** ⚠️ PARTIALLY VERIFIED
|
||||
- Prajna 2004 covers SOS optimization
|
||||
- Kapuria 2025 uses SMT solvers (Z3, dReal) — verified in dissertation
|
||||
- Kapuria 2025 uses SMT solvers (Z3, dReal) — verified in
|
||||
dissertation
|
||||
- **DANE: Verify Prajna specifically mentions SOS**
|
||||
|
||||
### Citation 29: frehse_spaceex_2011 (nondeterministic inputs)
|
||||
**Claim:** "While tools such as SpaceEx handle nondeterministic inputs"
|
||||
**Claim:** "While tools such as SpaceEx handle
|
||||
nondeterministic inputs"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- Section 3, p.4: "u(t) ∈ U, where... U ⊆ Rⁿ is a set of nondeterministic inputs"
|
||||
- Section 3, p.4: "u(t) ∈ U, where... U ⊆ Rⁿ is a set of
|
||||
nondeterministic inputs"
|
||||
- Exact match
|
||||
|
||||
### Citation 30: kapuria_using_2025 (STPA/UCA)
|
||||
**Claim:** "Kapuria demonstrates this process for SmAHTR, deriving uncertainty sets from unsafe control actions identified through STPA"
|
||||
**Claim:** "Kapuria demonstrates this process for SmAHTR,
|
||||
deriving uncertainty sets from unsafe control actions
|
||||
identified through STPA"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available
|
||||
- Abstract: "identifying unsafe control actions (UCAs) in cyber-physical systems"
|
||||
- Abstract: "identifying unsafe control actions (UCAs) in
|
||||
cyber-physical systems"
|
||||
- Section 1.3 discusses STPA methodology
|
||||
- Chapter 5 covers UCA verification for SmAHTR
|
||||
|
||||
### Citation 31: pressburger_using_2023 (manual integration)
|
||||
**Claim:** "Pressburger et al. identify manual translation from formal specifications to executable code as a significant source of implementation errors"
|
||||
**Claim:** "Pressburger et al. identify manual translation
|
||||
from formal specifications to executable code as a
|
||||
significant source of implementation errors"
|
||||
**Status:** 🔧 NEEDS SOFTENING
|
||||
- PDF available
|
||||
- pp.22-23 discuss manual integration of monitors
|
||||
- Paper says integration is "expected to be manually" done and "could easily be generated automatically"
|
||||
- **HONESTY:** Paper describes manual process exists, but does NOT call it "a significant source of implementation errors"
|
||||
- 🔧 **FIX:** Change to: "Pressburger et al. describe the manual integration process from formal specifications to executable code, noting opportunities for automation"
|
||||
- Paper says integration is "expected to be manually" done
|
||||
and "could easily be generated automatically"
|
||||
- **HONESTY:** Paper describes manual process exists, but
|
||||
does NOT call it "a significant source of implementation
|
||||
errors"
|
||||
- 🔧 **FIX:** Change to: "Pressburger et al. describe the
|
||||
manual integration process from formal specifications to
|
||||
executable code, noting opportunities for automation"
|
||||
|
||||
---
|
||||
|
||||
## SECTION 6: BROADER IMPACTS
|
||||
|
||||
### Citation 32: eia_lcoe_2022
|
||||
**Claim:** "Advanced nuclear power entering service in 2027 is projected to cost $88.24 per megawatt-hour... fixed O&M costs alone account for $16.15 per megawatt-hour"
|
||||
**Claim:** "Advanced nuclear power entering service in 2027
|
||||
is projected to cost $88.24 per megawatt-hour... fixed O&M
|
||||
costs alone account for $16.15 per megawatt-hour"
|
||||
**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV
|
||||
- This is EIA Annual Energy Outlook data
|
||||
- **DANE: Verify these exact figures ($88.24/MWh, $16.15/MWh) from EIA source**
|
||||
- Check if 2022 data is still the best available or if 2024/2025 exists
|
||||
- **DANE: Verify these exact figures ($88.24/MWh,
|
||||
$16.15/MWh) from EIA source**
|
||||
- Check if 2022 data is still the best available or if
|
||||
2024/2025 exists
|
||||
|
||||
### Citation 33: deroucy_ai_2025
|
||||
**Claim:** "Datacenter electricity consumption could reach 560 terawatt-hours by 2030—up from 4% to 13% of total national electricity consumption"
|
||||
**Claim:** "Datacenter electricity consumption could reach
|
||||
560 terawatt-hours by 2030—up from 4% to 13% of total
|
||||
national electricity consumption"
|
||||
**Status:** ✅ VERIFIED
|
||||
- PDF available (downloaded earlier)
|
||||
- p.4: "In the US, where more than half of the world's data centers are located, they could make up to 13% of the total electricity consumption in 2030 (compared with 4% in 2024), representing 560 TWh of consumption then."
|
||||
- p.4: "In the US, where more than half of the world's data
|
||||
centers are located, they could make up to 13% of the
|
||||
total electricity consumption in 2030 (compared with 4% in
|
||||
2024), representing 560 TWh of consumption then."
|
||||
- Exact quote match
|
||||
|
||||
### Citation 34: operator_statistics
|
||||
**Claim:** "Over 3,600 active NRC-licensed reactor operators work in the United States"
|
||||
**Claim:** "Over 3,600 active NRC-licensed reactor operators
|
||||
work in the United States"
|
||||
**Status:** ❌ CANNOT VERIFY — source unclear
|
||||
- **DANE: What is this source? NRC website? Verify the 3,600 figure is current**
|
||||
- **DANE: What is this source? NRC website? Verify the 3,600
|
||||
figure is current**
|
||||
|
||||
### Citation 35: 10CFR55
|
||||
**Claim:** "Divided into Reactor Operators (ROs) and Senior Reactor Operators (SROs)"
|
||||
**Claim:** "Divided into Reactor Operators (ROs) and Senior
|
||||
Reactor Operators (SROs)"
|
||||
**Status:** ✅ VERIFIED (regulatory citation)
|
||||
- 10 CFR 55 defines RO and SRO license types
|
||||
|
||||
### Citation 36: 10CFR50.54
|
||||
**Claim:** "Staffing requires at least two ROs and one SRO per unit"
|
||||
**Claim:** "Staffing requires at least two ROs and one SRO
|
||||
per unit"
|
||||
**Status:** ✅ VERIFIED (regulatory citation)
|
||||
- 10 CFR 50.54 covers operator staffing requirements
|
||||
- **DANE: Verify exact minimum staffing numbers (2 RO + 1 SRO) from regulation text**
|
||||
- **DANE: Verify exact minimum staffing numbers (2 RO + 1
|
||||
SRO) from regulation text**
|
||||
|
||||
---
|
||||
|
||||
@ -272,17 +401,22 @@ Legend:
|
||||
### ✅ VERIFIED (19 citations)
|
||||
- NUREG-0899, 10CFR50.34, 10CFR55.59, 10CFR55, 10CFR50.54
|
||||
- Kemeny1979, hogberg_root_2013
|
||||
- platzer_differential_2008, fulton_keymaera_2015, alur_hybrid_1993
|
||||
- katis_realizability_2022 (all uses), pressburger_using_2023 (case study use)
|
||||
- guernic_reachability_2009, mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017
|
||||
- platzer_differential_2008, fulton_keymaera_2015,
|
||||
alur_hybrid_1993
|
||||
- katis_realizability_2022 (all uses),
|
||||
pressburger_using_2023 (case study use)
|
||||
- guernic_reachability_2009, mitchell_time-dependent_2005,
|
||||
bansal_hamilton-jacobi_2017
|
||||
- frehse_spaceex_2011, branicky_multiple_1998
|
||||
- kapuria_using_2025, deroucy_ai_2025
|
||||
|
||||
### ⚠️ PARTIALLY VERIFIED / NEEDS CHECKING (8 citations)
|
||||
- WRPS.Description, gentillon_westinghouse_1999 — verify sources exist
|
||||
- WRPS.Description, gentillon_westinghouse_1999 — verify
|
||||
sources exist
|
||||
- baier_principles_2008 — standard definition, low risk
|
||||
- lunze_handbook_2009 — verify assume-guarantee language
|
||||
- meyer_strix_2018 — verify Mealy machine claim from full paper
|
||||
- meyer_strix_2018 — verify Mealy machine claim from full
|
||||
paper
|
||||
- katis_capture_2022 — verify parity game relevance
|
||||
- lang_formal_2021 — verify intractability claim
|
||||
- prajna_safety_2004 — verify SOS optimization claim
|
||||
@ -290,20 +424,25 @@ Legend:
|
||||
### ❌ CANNOT VERIFY (4 citations)
|
||||
- zhang_analysis_2025 — need PDF, verify 53%/92% figures
|
||||
- Kiniry2024 — need PDF, verify quotes
|
||||
- jacobs_reactive_2024 — need PDF (but low risk, standard definition)
|
||||
- jacobs_reactive_2024 — need PDF (but low risk, standard
|
||||
definition)
|
||||
- eia_lcoe_2022 — verify dollar figures current
|
||||
- operator_statistics — what source is this?
|
||||
|
||||
### 🔧 NEEDS FIXING (1 citation)
|
||||
- pressburger_using_2023 — soften "significant source of implementation errors" to "manual process that could be automated"
|
||||
- pressburger_using_2023 — soften "significant source of
|
||||
implementation errors" to "manual process that could be
|
||||
automated"
|
||||
|
||||
---
|
||||
|
||||
## PRIORITY ACTIONS FOR DANE
|
||||
|
||||
1. **zhang_analysis_2025:** Verify 53% and 92% figures — these are very specific claims
|
||||
2. **eia_lcoe_2022:** Confirm $88.24/MWh and $16.15/MWh are correct and current
|
||||
3. **operator_statistics:** What is this source? Verify 3,600 figure
|
||||
4. **10CFR50.54:** Confirm exact staffing requirement (2 RO + 1 SRO)
|
||||
5. **Kiniry2024:** Verify "most advanced" claim and exact quotes
|
||||
6. **lunze_handbook_2009:** Check for "assume-guarantee" language
|
||||
1. **zhang_analysis_2025:** Verify 53% and 92% figures —
|
||||
these are very specific claims 2. **eia_lcoe_2022:** Confirm
|
||||
$88.24/MWh and $16.15/MWh are correct and current 3.
|
||||
**operator_statistics:** What is this source? Verify 3,600
|
||||
figure 4. **10CFR50.54:** Confirm exact staffing requirement
|
||||
(2 RO + 1 SRO) 5. **Kiniry2024:** Verify "most advanced"
|
||||
claim and exact quotes 6. **lunze_handbook_2009:** Check for
|
||||
"assume-guarantee" language
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user