formal-methods

TLA

• tlaplus-jupyter

TLA+

• TLA+ in Practice and Theory (four-part blog post series by pressron)
• IronFleet@SOSP'2015
  • 唐瑞泽、谷晓松
• 谷晓松、唐瑞泽、纪业、易星辰

TLAPS

• Hyperbook
• TLA+ Version 2: A Preliminary Guide
• On Paxos
  • tlaps-examples/paxos
  • FM2016: Formal Verification of Multi-Paxos for Distributed Consensus
• 唐瑞泽、谷晓松、戴若石

SMT

Z3

• SAT/SMT by Examples
• 江雪、唐瑞泽、谷晓松、欧阳鸿荣、戴若石

Coq

• Software Foundations
• FRAP
• 江雪、唐瑞泽、谷晓松、戴若石

Boogie (Dafny)

• RALin

• LoopInvariant@CSUR'2014

• 张宇奇