FORMAL METHODS. I like to think of it as using mathematical rigor for reasoning about systems. Because mathematical reasoning and systems are such broad concepts, formal methods is an extremely broad field.
Formal methods is tied closely to:
- Logic
- Formal languages
- Automata Theory
- Control Theory
- Type Theory
- Theorem Proving
- Verification
Formal methods, in general, involves the specification, development, analysis, and verification of systems.
People
- Dustin Jamner
- Georgio Nicolas
- Nadim Kobeissi
- Bernd Finkbeiner
- Christoph Haase
- Max von Hippel
- Talia Ringer
- Shriram Krishnamurthi, work site
- ice1000, personal site
- Julia Belyakova
- Armando Solar-Lezama
- Adam Chlipala
Tools
Model Checkers
Theorem Provers/Proof Assistants
Links
- https://symbolic.software/
- Formal Security Analysis of the Signal Messaging Protocol
- From Program Verification to Synthesis
- Proof Assistant Stack Exchange
- MIT 6.512
- The Science of Deep Specificaiton
- en.wikipedia.org/wiki/Formal_verification
- The Invariant Game
- Software Foundations
- NEU Programming Research Laboratory
- Solving Hexiom with SAT
- IC3ref
- "A gently curated list of companies using verification formal methods in industry" - github.com/ligurio/practical-fm
Papers
(see local library)
- Using state machines to guide LLMs: arxiv.org/pdf/2307.09702v3.pdf
- Interaction Trees: arxiv.org/pdf/1906.00046.pdf
- Hardware Model Checking Competition: link
- Reducing state machines to sat: people.eecs.berkeley.edu/~alanmi/publications/other/tcad15_pdr.pdf
- Understanding IC3 (a SAT-based model checking algorithm): theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf
Concepts
- Markov Decision Processes: a model for decision making using states and probabilities. transitions are probabilities.
← home