Model Checking Reading Club/Baier, Katoen: Principles of Model Checking/01: System Verification

These pages contain remarks and comments – many typos and errata, some proposals for change – that we have found during reading the book:

Principles of model checking / Christel Baier; Joost-Pieter Katoen. – Cambridge, Mass.: MIT Press, 2008.

ISBN 978-0-262-02649-9.

For more details, see the table of contents.

Chapter 1: System Verification

• 1, 9, 10¹² million US dollars ] Is that correct? We would rather have thought something like 10¹² US dollars. – Please note that the notation of money is different from the notation on page 5.

• 1, -5, Pentium II ] Should be Pentium, see [1]. Jasper Berendsen

• 4, -6, 10 % to 15% ] spacing is inconsistent, read: 10% to 15%

• 5, 9, lines of code lines ] read: lines of code

• 5, footnote, much higher ] We couldn't see why the number stated in the footnote (5000 defects for Windows 95, which we estimated may have 5 M LoC) indicates a much higher defect rate than normal. David Jansen

• 6, 4, Pentium II ] Should be Pentium, see [2]. Jasper Berendsen

• 10, -2, (viz. -1) ] read LaTeX code: (viz.\@ $-1$)

• 13, 14, physical limits of the computer memory. ] or, limits of the designer's patience. David Jansen

• 14, section 1.2.2, bullet 4 ] Model checkers provide diagnostic information only for failures of universally quantified properties. For existentially quantified properties, doing so would generally require displaying a proof. Tim Leonard
• 14sq., list of strengths of model checking ] almost all, but not all points have one or two words italicised.