Wiki

• Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics.
• Software verification goal is to assure that software satisfies the expected requirements.
• F* (programming language) is a high-level, multi-paradigm, functional and object-oriented programming language inspired by the languages ML, Caml, and OCaml, and intended for program verification.
  • функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ.

Books

• Introducing Software Verification with Dafny Language. Proving Program Correctness by Boro Sitnikovski - 131 pages

Logic: The Calculus of Computation 🔗

• Aaron Bradley
  • flyer.pdf
  • slides
    • cs156
      • all-4.pdf
  • Books
    • The Calculus of Computation: Decision Procedures with Applications to Verification
    • Programming for Engineers
• ACM SIGACT News: Vol 42, No 1 / Review of The calculus of computation: decision procedures with applications to verification by Aaron R. Bradley and Zohar Manna by Carlo A. Furia
• Nelma Moreira
  • The Calculus of Computation. Decision Procedures with Applications to Verification by Aaron R. Bradley · Zohar Manna
• K. Subramani, Ph. D.
  • The Calculus of Computation. Decision Procedures with Applications to Verification by Aaron R. Bradley · Zohar Manna

Papers

• Social Processes and Proofs of Theorems and Programs by Richard A. De Millo, Richard J. Lipton and Alan J. Perlis
  • Bjarne Stroustrup