Table of contents for Calculus of computation : decision procedures with applications to verification / Aaron R. Bradley, Zohar Manna..


Bibliographic record and links to related information available from the Library of Congress catalog
Note: Electronic data is machine generated. May be incomplete or contain other coding.


Counter
Part I Foundations
I   Propositional Logic ..................   ...................  3
1.I Syntax ........................................ ..... .4
1.2  Semantics  ...............................................  6
1.3 Satisfiability and Validlidity ..... ........................... 8
1.3.1  Truth  Tables .................................. ....  9
1.3.2  Semantic Arguments  ............................  10
1.4  Equivalence and Implication .............................. 14
1.5  Substitution  ............ ........ ...............     16
1.6  Normal Forms  .............................. .............
1.7 Decision Procedures for Satisfiability ...................... 21
1.7.1  Simple Decision  Procedures ........................  21
1.7.2 Reconsidering the T'ruth-Table Method. .............. 22
1.7.3 Conversion to an Equisatisfiable Formula in CNF ...... 24
1.7.4  The Resolution  Procedure ......................  ...  27
1.7.5 DPILL............................. ........... 28
1.8 Summary ............................................. 31
Bibliographic Remarks ...................................... 32
Exercises ................................................. 32
2   First-Order Logic .................. ..................... ..35
2.1 Syntax ..............................    ...... .    ..... 35
2.2  Senantics  ......... ................... .................  39
2.3 Satifiability and Validity ................... ............. 42
2,4 Substitution ................... ..................... ......
2.4.1  Safe  Substitution  ...................... ........ .  47
2.1.2  Schem a  Substitution  ............. ...... ..........  18
"2.5 Normal Forms . . ...................................  . 51
2.6 Decidabilitv and Complexity ................... ........ 53
2.6.1  Satisfiability as a Formal Language  ............  .....  53
06.2   Decid ility  ...............   ...............       ...  54
2.6.3  *  ( m ple ity  ....................................  54-
27   *   pl:t  I Ieorenis of First--Order Logic ..............   ... 56
I  Simplifving t he Language' o, FOL .... ............. 57
2. 2  SnuM.ntic Argumtent Proof Rules . .u.. . . .....  ..... 58
1.7    Sm        an untnss and Comrnpletenes.s ........  ........   58
7.1    Addltional Theorems ......... ..................... 61
58  S in  lary ..............   ..............................   66
ilig   raphic  Remark ....... ......................   ........ .  67
E i  'ci st s   . ... . .. .. .. .. .. . . ... ... ... .. ..  . .... . ..  6 7
3   List -O)rder Theories ......       ........................... 69
;ii  rst -(rdtict  rsion ........... 271
2.1 Phase 1: Variable Astra,ctn ..         ...     ...2....  71
1i2.2 thase 2: Guess amnil (Chek .........................273
1i.23    atid    cic      ..................      .......271
i      i Nels o-()-ppei  Melthr : Di  termini stic   rsi   ........  ......  276
10. 31 ( ivs T I heoris   ............................. 276
10.3 2 Phase 2: Equality Propagation ..................... 278
1It.3.3 E1 tiaits Pro pagatioi In pliemtatLion ...............282
i ti I *( trtr ct ness oC t he NeEsontt-Oppet Methlo.   .        28:3
S         l  v  ...... ................................       ...  287
t:     ric     ar   ................. .........       .........288
S      t t:rt Hcis   ... s  .   . ...  .     . ........          288
SArrs        .   .................     ............................291
li     ATa,ys with  { ninterpreted  Inii  es ........ ................ 292
I l.l irairts Pr'etioy  Fra.git to         ........ 292
1.1 .2 Decision Prieie ...........        ..... ....... ...294
l   tte tr-l  i  Ar  is ...............  .......  ...........  299
11.2.1  Array  Proprt  Fragnmenit  .........................  300
11.2.2 D-ecision ProcrPdure ...........................  . . 301
11.3 Ha>shItables   .......        ....  ..........    ....... 30-4
1 [.3  1  Hashtable Property  Fragment ......................  305
11.3.2  Decision  Procedure  ................... .......... .  306
11    Larger Fragments  ....................... .............. . 3018
1l.5  Summary .....          .       ...  ...................   30!
i  liographic  Rem arks ................... ...........  ......... 310
[-xercises    .....            ............             .......  310
12  Invariant Generation ...................................... 311
12.1 Invari ant (Generation .  ................. .................. 311
12.1.1 VWe(kest Pre(cotniition and Strongest Postcondition .... 312
12.1.'2 *Ceneral Definitions of wp and sp ........ ......... 315
12.1.3 Static Analysis .............. ...................  316
12.1.1 Abstraction. .........          .....................319
12.2 Interval Alalsis ....... ............................... 325
1 2.3  Karr's  Analysis. . .. ..... ....  .. ................ .   ......   333
12.4 *Standlard Notation and Cnceepts ........... .....  ........ 341
12.5 Snummary ............................. ......   ......... 344
Bibliographic  emarks .............. ........   .............. 345
E xercises  .......... . ......... ...................    ..... 345
13  Further Reading ................. ........ .     .....    ... .3147



Library of Congress subject headings for this publication: Computer logic, Computer programs Verification