/Formal-Methods-Materials

A Short Introduction to Formal Methods

Apache License 2.0Apache-2.0

  • [1. Applied Machine Learning for Program Verification]

    • [1.1 Model Checking]

    • LTL

    • CTL

    • Bounded Model Checking

    • Unbounded Model Checking

    • [1.2 Loop Invariant Synthesis]

    • Counterexample-Guided Synthesis

    • Syntax-Guided Synthesis

    • Template-Guide Synthesis

    • Property Reachability Synthesis

    • Deep Learning-based Synthesis

    • Other Synthesis Methods

    • [1.3 Hoare Logic and Separation Logic]

    • Hoare Logic

    • Separation Logic

    • [1.4 SAT, SMT and CHC Solver]

    • SAT

    • SMT

    • CHC Solver

    • [1.5 Automated Theorem Proving]

    • HOL

    • FOL

    • Coq

    • Isabelle

    • Why3

    • Lean

    • [1.6 Program Synthesis and Repair]

  • [2. Unsorted Online Sources]

2. Unsorted Online Sources

2.1. Courses

  • "Bug Catching: Automated Program Verification", Matt Fredrikson, 2023, CMU [link]
  • "程序语言理论与实现", 张宏波, 2022, courses [link]
  • "软件科学基础", 熊英飞, 2022, PKU [link]
  • "软件分析技术（Software Analysis）", 熊英飞, 2022, PKU [link]
  • "软件分析与验证", 贺飞, 2022, THU [link]
  • "Static Program Analysis", Yue Liand Tian Tan, 2022, NJU [link]
  • "程序验证 专栏", FRONTIERS, 2022, 知乎 [link]
  • "CS 357 Advanced Topics in Formal Methods", Aleksandar Zeljić, 2022, Stanford [link]
  • "CSC2547HS Winter 2023 Automated Reasoning with Machine Learning", Xujie Si, 2023, University of Toronto [link]
  • "PROOF AUTOMATION", TALIA RINGER, 2022, University of Illinois Urbana-Champaign [link]
  • "6.826: Principles of Computer Systems", 2020, MIT [link]
  • "CSE 507: Computer-Aided Reasoning for Software", Emina Torlak, 2022, UW [link]
  • "Logic and Mechanized Reasoning", Marijn Heule and Jeremy Avigad, 2021, PKU [link]
  • "Automated Logical Reasoning", Işıl Dillig, 2022, University of Texas [link]
  • "CS156: The Calculus of Computation, Winter 2010", Zohar Manna, 2010, Stanford [link]
  • "EECS 219C: Formal Methods: Specification, Verification, and Synthesis", Sanjit A. Seshia, 2023, UCB [link]
  • "Summer Seminar: Computer-Aided Verification", 2017, Shanghaitech [link]
  • "ECE.750t29f18 Automated Program Verification", Arie Gurfinkel, 2023, University of Waterloo [link]