Concrete Semantics is an excellent free book http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ written by some well-known names in the field

Concrete Semantics is an excellent free book http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ written by some well-known names in the field. It's a good place to begin. The book itself contains references to much more advanced works such as Nielson & Nielson or TAPL. It doesn't cover one part of formal methods, (probabilistic) model checking.