fm

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

• Verifpal
• Linear Temporal Logic
• compcert
• Haskell
• CakeML

Model Checkers

• Spin
• TLA+
• NuSMV

Theorem Provers/Proof Assistants

• Coq
- Ltac
• Lean Theorem Prover
• ACL2
- ACL2s
• Isabelle
• Agda
• SASyLF

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.