Formal-Methods

• Differential Privacy: Formal Guarantees, Composition Theorems, and the Engineering of Private Systems · 2025-08-12

  Build differential privacy from first principles: the formal (ε, δ)-definition, the Laplace and Gaussian mechanisms, composition theorems (basic and advanced), the sparse vector technique, and how to engineer practical private data systems at scale.

• Memory Consistency Models: From Sequential Consistency to the C++11 Memory Model · 2025-06-24

  A rigorous treatment of memory consistency models: Lamport's sequential consistency, the transition to relaxed models, the formal semantics of the C++11 memory model with its acquire-release and relaxed atomics, and how to reason about concurrent code that doesn't tear.

• Linearizability and Serializability: A Formal Hierarchy of Consistency Models · 2025-01-28

  Build a rigorous understanding of consistency models from linearizability to eventual consistency, with formal definitions, counterexamples, and the practical implications for distributed database design.

• Separation Logic: The Frame Rule, Separating Conjunction, and Concurrent Verification · 2022-01-01

  An exploration of separation logic—O'Hearn and Reynolds's revolutionary extension of Hoare logic for local reasoning about mutable state, the frame rule, and concurrent separation logic.

• Abstract Interpretation: Cousot's Galois Connection Framework, Widening/Narrowing, and Sound Static Analysis by Construction · 2021-12-29

  A deep exploration of abstract interpretation—the mathematical theory of sound approximation that underpins every modern static analyzer, from the Astrée system to the Rust borrow checker.