diff --git a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/ME 2150 - High Assurance Cyber-Physical Systems - README.md b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/ME 2150 - High Assurance Cyber-Physical Systems - README.md index d9518daf0..ebfd138b8 100644 --- a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/ME 2150 - High Assurance Cyber-Physical Systems - README.md +++ b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/ME 2150 - High Assurance Cyber-Physical Systems - README.md @@ -5,6 +5,7 @@ - [[2025-01-14 Microkernels.md]] - [[2025-01-16 HACMS Program Overview.md]] - [[2025-02-18 Boyd Talk.md]] +- [[2025-03-25 Max's Lecture.md]] - [[Capabilities Tutorials.md]] - [[Investigating seL4 with Docker.md]] - [[Lean.md]] @@ -14,24 +15,5 @@ - [[!Things That Need Done.md]] ## Summary -It appears that you have a collection of notes and to-do lists from a course on High Assurance Cyber-Physical Systems (ME 2150) at Carnegie Mellon University. The notes cover various topics, including: - -1. A lecture by Jeremy Avigad on Lean, a formal system for reasoning about mathematics. -2. A talk by Boyd Mutlerer on SeL4, Kry10, and the concept of "KOS" (which he doesn't like). -3. To-do lists for completing the course material, including: - * Completing the seL4 tutorials - * Working through the Microkit tutorial - * Reading parts 1-3 of the Microkit tutorial - * Attempting to complete parts 2-4 of the Microkit tutorial (status: not started) - * Starting an introduction to SeL4 proofs - -Some notable observations from these notes: - -* The importance of evidence in science and engineering is emphasized, particularly when it comes to software verification. -* The use of formal systems like Lean and SeL4 for reasoning about mathematics and computer systems is highlighted. -* The concept of the "innovator's dilemma" is mentioned, which suggests that as technology advances, new challenges and trade-offs emerge. -* The value of interactive theorem provers (ITPs) like ITP is discussed. - -Overall, these notes suggest a focus on formal methods, software verification, and high-assurance systems in the context of computer science and engineering. Generated by llama3.2:latest