I’ve posted this as Lobsters has a sub-community that has shown a lot of interest in formal methods.

Formal methods have been historically quite unfriendly, as @hwayne has discussed in many of his insightful comments and blogposts.

The authors of this book, Nielson & Nielson, wrote the standard textbook on static analysis. I find it very interesting that they are writing a more introductory volume where they trade some generality for simplicity. They use program graphs as the basic data structure to build different formal methods on, and the resulting textbook is quite approachable!

I’ve posted this as Lobsters has a sub-community that has shown a lot of interest in formal methods.

Formal methods have been historically quite unfriendly, as @hwayne has discussed in many of his insightful comments and blogposts.

The authors of this book, Nielson & Nielson, wrote the standard textbook on static analysis. I find it very interesting that they are writing a more introductory volume where they trade some generality for simplicity. They use program graphs as the basic data structure to build different formal methods on, and the resulting textbook is quite approachable!

There’s also a companion website with runnable formal methods: http://www.formalmethods.dk/

I did cover some alternative textbooks in a comment I posted a year ago: https://lobste.rs/s/3hj7gs/using_z_specification_refinement_proof#c_5dayun

There is also a second volume by the same authors, freely available on arXiv: https://arxiv.org/pdf/2012.10086.pdf