logoalt Hacker News

rramadass • today at 12:48 PM • 0 replies • view on HN

Mandatory Background:

1) Understanding Formal Methods by Jean-Francois Monin - This is the absolute best for getting a grip on the breadth, concepts and sample tools for Formal Mathematics/Specification/Verification. Fire-hose of information (not a step-by-step textbook) so use this as a map for everything "Formal". The S/N ratio is very high (~250 pages only!) so use AI/Textbooks to help explain concepts you find difficult to understand.

Practical:

1) Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - Uses "Alloy" language to teach Structural (i.e. Data) Modeling.

2) Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport - Uses "TLA+" language to teach Behavioural (i.e. State Machine) modeling.

The above two are for "System Modeling" i.e. everything needed to formally build complete systems.

3) Finally, You should also look at the bunch of free books on the Lean4 website which can be studied parallely for "code-level" proofs and verification.

PS: There are a few more (eg. Event-B method etc.) but you can get to those if/when you need to.