diff --git a/201 Metadata/My Library.bib b/201 Metadata/My Library.bib
index 2718bf0eb..b3e1d8a72 100644
--- a/201 Metadata/My Library.bib	
+++ b/201 Metadata/My Library.bib	
@@ -6595,6 +6595,24 @@ Regulatory Premises.pdf}
   file = {/home/danesabo/Zotero/storage/XNCF39K8/Klein et al. - 2018 - Formally verified software in the real world.pdf}
 }
 
+@article{kleinFormallyVerifiedSoftware2018a,
+  title = {Formally Verified Software in the Real World},
+  author = {Klein, Gerwin and Andronick, June and Fernandez, Matthew and Kuz, Ihor and Murray, Toby and Heiser, Gernot},
+  date = {2018-09-26},
+  journaltitle = {Communications of the ACM},
+  shortjournal = {Commun. ACM},
+  volume = {61},
+  number = {10},
+  pages = {68--77},
+  issn = {0001-0782, 1557-7317},
+  doi = {10.1145/3230627},
+  url = {https://dl.acm.org/doi/10.1145/3230627},
+  urldate = {2024-11-11},
+  abstract = {Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.},
+  langid = {english},
+  file = {/home/danesabo/Zotero/storage/EUFBUXNE/Klein et al. - 2018 - Formally verified software in the real world.pdf}
+}
+
 @inproceedings{kleinSeL4FormalVerification2009,
   title = {{{seL4}}: Formal Verification of an {{OS}} Kernel},
   shorttitle = {{{seL4}}},
@@ -11735,6 +11753,22 @@ Subject\_term: Careers, Politics, Policy},
   file = {/home/danesabo/Zotero/storage/T9L6LJMI/Sun et al. - 2021 - SoK Attacks on Industrial Control Logic and Forma.pdf;/home/danesabo/Zotero/storage/VSLPZVKJ/Sun et al. - 2021 - SoK Attacks on Industrial Control Logic and Forma.pdf;/home/danesabo/Zotero/storage/4KZGCWIW/2006.html}
 }
 
+@online{sunSoKAttacksIndustrial2021a,
+  title = {{{SoK}}: {{Attacks}} on {{Industrial Control Logic}} and {{Formal Verification-Based Defenses}}},
+  shorttitle = {{{SoK}}},
+  author = {Sun, Ruimin and Mera, Alejandro and Lu, Long and Choffnes, David},
+  date = {2021-03-23},
+  eprint = {2006.04806},
+  eprinttype = {arXiv},
+  eprintclass = {cs},
+  url = {http://arxiv.org/abs/2006.04806},
+  urldate = {2024-11-11},
+  abstract = {Programmable Logic Controllers (PLCs) play a critical role in the industrial control systems. Vulnerabilities in PLC programs might lead to attacks causing devastating consequences to the critical infrastructure, as shown in Stuxnet and similar attacks. In recent years, we have seen an exponential increase in vulnerabilities reported for PLC control logic. Looking back on past research, we found extensive studies explored control logic modification attacks, as well as formal verification-based security solutions. We performed systematization on these studies, and found attacks that can compromise a full chain of control and evade detection. However, the majority of the formal verification research investigated ad-hoc techniques targeting PLC programs. We discovered challenges in every aspect of formal verification, rising from (1) the ever-expanding attack surface from evolved system design, (2) the real-time constraint during the program execution, and (3) the barrier in security evaluation given proprietary and vendor-specific dependencies on different techniques. Based on the knowledge systematization, we provide a set of recommendations for future research directions, and we highlight the need of defending security issues besides safety issues.},
+  pubstate = {prepublished},
+  keywords = {Computer Science - Cryptography and Security},
+  file = {/home/danesabo/Zotero/storage/ZM8DBCRX/Sun et al. - 2021 - SoK Attacks on Industrial Control Logic and Formal Verification-Based Defenses.pdf;/home/danesabo/Zotero/storage/63DKNBDF/2006.html}
+}
+
 @article{symb,
   title = {The {{Comprehensive LaTeX Symbol List}}},
   author = {Pakin, Scott},