Zulip Chat Archive

Stream: new members

Topic: Software verification tutorials?

Ypres (Jan 22 2023 at 04:56):

I am exploring Lean and I was wondering if there are any software verification tutorials, textbooks or reviews/articles that explain how to use Lean in the context of software verification?

I know about The Hitchhicker's Guide to Logical Verification. This is heavily inspired by Concrete Semantics, an Isabelle/HOL book. In turn, Concrete Semantics is a formalization of most material discussed in The Formal Semantics of Programming Languages. This is a classic textbook on semantics, but it is a bit too theoretical.

Coq has Software Foundations and Formal Reasoning about Programs, which are quite practical. They discuss e.g. lots of embedding or stepwise refinement techniques, just to name two things used to verify large software artifacts.

Last updated: Dec 20 2023 at 11:08 UTC