Ancillary Material: some figures, programs and URLs from our book

• page 14: Figure 1.1
• page 34: Figure 1.3
• page 36: Figure 1.4
• page 37: Figure 1.5
• page 38: Figure 1.6
• page 40: Figure 1.7
• page 40: Figure 1.8
• page 42: Figure 1.9
• page 44: Figure 1.10
• page 50: Figure 1.11
• page 60: function CNF
• page 61: function DISTR
• page 62: function NNF
• page 67: function HORN
• page 70: Figure 1.12
• page 70: Figure 1.13
• page 71: Figure 1.14
• page 72: Figure 1.15
• page 73: Figure 1.16
• page 74: Figure 1.17
• page 75: Figure 1.18
• page 76: Figure 1.19
• page 77: Figure 1.20
• page 82: Figure 1.21
• page 83: Figure 1.22
• page 84: Figure 1.23
• page 101: Figure 2.1
• page 104: Figure 2.2
• page 105: Figure 2.3
• page 107: Figure 2.4
• page 137: Figure 2.5
• page 145: Figure 2.6
• page 145: Figure 2.7
• page 146: Figure 2.8
• page 147: Figure 2.9
• page 147: Figure 2.10
• page 148: Figure 2.11
• page 152: Figure 2.12
• page 153: StructurallyEqual
• page 154: Figure 2.13
• page 159: Figure 2.14
• page 168: Figure 2.15
• page 170: www.comlab.ox.ac.uk/oucl/users/bernard.sufrin/jape.html
• page 171: http://www-2.cs.cmu.edu/~fp/courses/comp-ded/
• page 176: Figure 3.1
• page 177: Figure 3.2
• page 179: Figure 3.3
• page 179: Figure 3.4
• page 180: Figure 3.5
• page 181: Figure 3.6
• page 188: Figure 3.7
• page 191: Figure 3.8
• page 192: an SMV program
• page 193: Figure 3.9
• page 193: a bit counter
• page 196: Figure 3.10
• page 198: Figure 3.11
• page 200: Figure 3.11
• page 202: Figure 3.13
• page 204: Figure 3.14
• page 205: Figure 3.15
• page 206: Figure 3.16
• page 207: Figure 3.17
• page 210: Figure 3.18
• page 212: Figure 3.19
• page 213: Figure 3.20
• page 213: Figure 3.21
• page 214: Figure 3.22
• page 219: Figure 3.23
• page 223: Figure 3.24
• page 224: Figure 3.25
• page 225: Figure 3.26
• page 226: Figure 3.27
• page 227: Figure 3.28
• page 228: Figure 3.29
• page 228: Figure 3.30
• page 229: Figure 3.31
• page 232: Figure 3.32
• page 233: Figure 3.33
• page 233: Figure 3.34
• page 236: Figure 3.35
• page 238: Figure 3.36
• page 240: Figure 3.37
• page 245: Figure 3.38
• page 246: Figure 3.39
• page 248: Figure 3.40
• page 249: Figure 3.41
• page 253: Figure 3.42
• page 254:
  • www.cs.cmu.edu/~modelcheck/
  • http://nusmv.irst.itc.it
  • www-cad.eecs.berkeley.edu/~kenmcmil/
  • http://patterns.projects.cis.ksu.edu/
  • netlib.bell-labs.com/netlib/spin/whatispin.html
  • http://www.fsel.com/fdr2_download.html
• page 255:
  • http://www.dcs.ed.ac.uk/home/cwb
  • http://www.cs.sunysb.edu/~cwb/
  • http://bogor.projects.cis.ksu.edu/
• page 305:
  • http://www.opensource.org
  • http://www.sims.berkeley.edu/~pam/papers.html
• page 308: Figure 5.1 (left)
• page 308: Figure 5.1 (right)
• page 309: Figure 5.2
• page 311: Figure 5.3
• page 312: Figure 5.4
• page 315: Figure 5.5
• page 317: Table 5.6
• page 318: Table 5.7
• page 321: Table 5.8
• page 323: Figure 5.9
• page 323: Figure 5.10
• page 324: Figure 5.11
• page 325: Table 5.12
• page 336: Figure 5.12
• page 356: http://www.cis.ksu.edu/~allen/porgi.html
• page 361: Figure 6.1
• page 361: Figure 6.2
• page 362: Figure 6.3 (left)
• page 362: Figure 6.3 (right)
• page 363: Figure 6.4
• page 364: Figure 6.5 (left)
• page 364: Figure 6.5 (right)
• page 365: Figure 6.6 (left)
• page 365: Figure 6.6 (right)
• page 366: Figure 6.7
• page 367: Figure 6.8
• page 367: Figure 6.9
• page 368: Figure 6.10
• page 370: Figure 6.11
• page 371: Figure 6.12
• page 371: Figure 6.13
• page 373: Figure 6.14
• page 375: Figure 6.15
• page 376: Figure 6.16
• page 376: Figure 6.17
• page 378: Figure 6.18
• page 378: Figure 6.19
• page 379: Figure 6.20
• page 379: Figure 6.21; may require macros: \def\bddFigFontSize{7} \newcommand{\Exx}[1]{$\stackrel{\exists x_{#1}}{\Rightarrow}$}
• page 380: Figure 6.22
• page 380: Figure 6.23
• page 384: Figure 6.24
• page 384: Figure 6.25
• page 385: Figure 6.26
• page 386: Figure 6.27
• page 387: Figure 6.28
• page 389: Figure 6.29
• page 403: Figure 6.30 (left)
• page 403: Figure 6.30 (right)
• page 404: Figure 6.31
• page 407: Figure 6.32 (left)
• page 407: Figure 6.32 (right)
• page 408: Figure 6.33