38 lines
1.9 KiB
Markdown
38 lines
1.9 KiB
Markdown
# Table of Contents for ME 2150 - High Assurance Cyber-Physical Systems
|
|
|
|
## Files
|
|
- [[2025-01-09 Syllabus and Introduction.md]]
|
|
- [[2025-01-14 Microkernels.md]]
|
|
- [[2025-01-16 HACMS Program Overview.md]]
|
|
- [[2025-02-18 Boyd Talk.md]]
|
|
- [[Capabilities Tutorials.md]]
|
|
- [[Investigating seL4 with Docker.md]]
|
|
- [[Lean.md]]
|
|
- [[ME 2150 - High-Assurance Cyber-Physical Systems Homework 1 Complete.md]]
|
|
- [[ME 2150 - High-Assurance Cyber-Physical Systems Homework 1.md]]
|
|
- [[press.png]]
|
|
- [[!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
|