Automated Reasoning International Joint Conference IJCAR2008

Software Verification: Roles and Challenges for Automatic Decision Procedures......Page 12
Introduction......Page 13
Extended Real Numbers......Page 15
Interval Arithmetic......Page 16
Bounds on Real-Valued Functions......Page 17
Floating-Point Arithmetic......Page 18
Straight-Line Programs......Page 20
Converting Terms......Page 21
Proving Propositions......Page 22
Bisection and Refined Evaluation......Page 23
Remez' Polynomial of the Square Root......Page 24
Relative Error for an Elementary Function......Page 25
Conclusion......Page 26
Introduction......Page 29
Logic......Page 30
Interpretation......Page 31
Atoms......Page 32
Correctness......Page 33
Atoms......Page 34
The Interior Point Method......Page 35
A Verified Implementation of the Interior Point Method......Page 36
The Method of Infinitesimals......Page 37
Atoms......Page 38
Ferrante and Rackoff......Page 39
Presburger Arithmetic......Page 40
Cooper's Algorithm......Page 41
Correctness......Page 42
Related Work......Page 43
Introduction......Page 45
Related Work......Page 46
Definitions......Page 47
Motivating Example......Page 49
Model Theoretic Method......Page 50
Symbolic Shape Graphs......Page 51
Symbolic Graph Representations......Page 53
From Formulae to Sets of SGR......Page 56
Application of the Model Theoretic Method for QSL......Page 58
Conclusions......Page 59
Introduction......Page 61
Binary Relations and Relation Algebras......Page 62
Boolean Algebras: A Warm-Up......Page 63
Boolean Algebras with Operators......Page 64
Relation Algebras......Page 66
Functions, Vectors and Other Concepts......Page 68
Abrial's Relatives......Page 70
Simulation Laws for Data Refinement......Page 71
Outlook......Page 74
Conclusion......Page 75
Relation Algebra in TPTP-style......Page 77
Introduction......Page 78
Formal Preliminaries......Page 79
Array-Based Systems and Their Symbolic Representation......Page 80
Symbolic Representation of States and Transitions......Page 82
Symbolic Representation and SMT Solving......Page 85
Backward Reachability......Page 87
Termination of Backward Reachability......Page 89
Progress Formulae for Recurrence Properties......Page 90
Related Work and Conclusions......Page 92
Introduction......Page 94
Related Work......Page 95
Setting......Page 96
Verification Condition Generation......Page 98
Preservation of Proof Obligations......Page 107
Practical Issues......Page 108
Conclusion......Page 109
Introduction......Page 111
Eliminating Ill-definedness......Page 113
Defining the $D$ Operator......Page 114
An Approximation of the $D$ Operator......Page 115
Syntactical Derivation of $Y$......Page 116
Implementation and Empirical Results......Page 117
Related Work......Page 119
Conclusion......Page 121
Semantic Proof of Equivalence......Page 123
Introduction......Page 127
Running Example......Page 129
Model......Page 130
Reducing $I$ to $DY$......Page 132
The Automaton Model......Page 135
Encoding Infinite Signatures......Page 136
Coping with Associativity and Commutativity of xor and mult.......Page 137
Closure under DY and Compatibility with the Closure under AC......Page 138
Example......Page 139
Conclusion......Page 140
Introduction......Page 143
Methods That Directly Classify Polytime......Page 144
Implementation......Page 146
Experiments and Conclusions......Page 148
Introduction......Page 150
Description of the LogAnswer System......Page 151
Theorem Provers of LogAnswer......Page 154
Conclusions and Future Work......Page 156
Background......Page 158
Examples and System Walk-Through......Page 160
Implementation......Page 161
Conclusions and Further Work......Page 164
The Logic Underlying Abella......Page 165
Specification Logic......Page 167
Implementation......Page 168
Examples......Page 169
Future and Related Work......Page 170
Introduction and Motivation......Page 173
Overview of LEO-II......Page 174
Cooperative Proof Search......Page 175
Term Sharing and Term Indexing......Page 178
Conclusion......Page 179
Introduction......Page 182
KeYmaera Verification Tool for Hybrid Systems......Page 183
Hybrid Systems, Hybrid Automata, and Hybrid Programs......Page 184
Syntax and Semantics of Differential Dynamic Logic......Page 185
Real Arithmetic and Computer Algebra......Page 186
Parameter Discovery......Page 187
Related Work......Page 188
Introduction......Page 190
Rooted Query Entailment in \ALCI and \SHIQ......Page 192
2ExpTime-Hardness Results......Page 198
Query Entailment in \SHQ is ExpTime-Complete......Page 200
Conclusion......Page 203
Introduction......Page 205
General Framework......Page 207
A Mainstream Description Logic with Transitive Roles......Page 212
A Description Logic with Boolean Role Operators......Page 213
Discussion......Page 217
Introduction......Page 221
Hybrid Logic with D and Converse......Page 223
Tableau Rules......Page 224
Control......Page 226
Termination......Page 228
Model Existence......Page 230
Conclusion......Page 234
Introduction......Page 237
The Description Logic \SI......Page 239
Basic Definitions for Pinpointing......Page 240
Looping Tree Automata......Page 241
The General Approach......Page 243
Constructing Axiomatic Automata for \SI......Page 245
Computing the Behaviour of a WLA......Page 247
Conclusions......Page 251
Introduction......Page 253
Preliminaries......Page 254
Motivation......Page 255
The Standard Hypertableau Calculus for \SHOIQ......Page 256
Introducing Individual Reuse......Page 258
The \ELOH Case......Page 262
The General Case......Page 264
Evaluation......Page 265
Conclusion......Page 267
References......Page 268
Introduction......Page 270
Preliminaries......Page 271
Basic Properties of \EL......Page 273
Deciding $\Sigma$-Entailment: Theory......Page 274
Practical Algorithm and System......Page 279
Experimental Evaluation......Page 280
Uniform Interpolation......Page 282
Discussion......Page 283
Introduction......Page 286
Aligator - Underlying Principles......Page 287
Inside Aligator - Main Steps of the Tool......Page 288
Conclusions......Page 293
Introduction......Page 294
Architecture......Page 295
Performance......Page 296
Architecture......Page 298
Performance......Page 299
Conclusion......Page 301
Introduction......Page 303
Instantiation Calculus......Page 304
Redundancy Elimination......Page 305
Saturation Algorithm: The Inst-Gen Loop......Page 306
References......Page 309
Introduction......Page 310
Various Caching Methods......Page 311
Problem Sets, Experiments and Results......Page 312
Conclusions and Further Work......Page 315
Introduction......Page 317
Inference System......Page 318
Implementation......Page 320
Interface......Page 321
Experimental Results......Page 322
Introduction......Page 324
Proving Termination by Transformation......Page 326
Proving Termination of Rewrite Theories with MTT......Page 327
Implementation of the Tool......Page 328
Introduction......Page 331
Example......Page 332
Celf......Page 333
Conclusion......Page 336
Background......Page 338
Theory of Canonicity......Page 339
Applications of Canonicity......Page 340
Introduction......Page 343
Preliminaries......Page 344
Background......Page 346
Atomic String-Rewriting Systems......Page 348
Bit-Swapping Systems......Page 351
Leaf-Permutative Presentations......Page 353
Conclusion......Page 357
Introduction......Page 359
Preliminaries......Page 360
Modularity of Confluence, by Decreasing Diagrams......Page 363
Modularity of Confluence, Constructed......Page 369
Constructor-Sharing TRSs......Page 371
Extra-Variable TRSs......Page 372
Conclusion......Page 373
Introduction......Page 375
Preliminaries......Page 377
The Dependency Pair Method......Page 378
Usable Rules......Page 381
The Weight Gap Principle......Page 383
Reduction Pairs and Argument Filterings......Page 385
Experiments......Page 388
Conclusion......Page 389
Introduction......Page 391
Background......Page 393
Direct Systems......Page 395
Computing Minimal Models......Page 398
Direct-Optimal Systems......Page 400
Rewrite-Optimality......Page 402
Discussion......Page 405
Introduction......Page 407
Intruder Deductions......Page 408
Bounded Number of Sessions......Page 410
Clausal Theorem Proving and Security Protocols......Page 412
Proofs of Equivalences......Page 414
Modularity......Page 415
Introduction......Page 421
Preliminaries......Page 422
Inference Rules......Page 424
Soundness, Completeness and Complexity......Page 427
Simultaneous Propagation and FUIP-Based Conflict Resolution......Page 428
Selecting Decision Literals and Substitution Sets......Page 431
Hybrid Substitution Sets......Page 432
Implementation and Evaluation......Page 433
Conclusions......Page 434
Introduction......Page 437
Propositional vs First-Order Resolution......Page 438
The Generalisation Inference Rule......Page 440
Sort Inference for Generalisation......Page 442
Generalisation vs Resolution......Page 444
Conclusion and Future Work......Page 449
Introduction......Page 452
Machine Learning Axiom Relevance......Page 453
Semantic Relevance Axiom Selection......Page 454
Combining Machine Learning with Semantic Selection......Page 456
Detailed Example......Page 458
Partial vs. Total Models......Page 461
Term Structure......Page 462
Results......Page 463
Future Work and Conclusion......Page 465
CASC-J4 The 4th IJCAR ATP System Competition......Page 468
Introduction......Page 470
Labelled Splitting......Page 471
Experiments......Page 482
Related Work......Page 483
Conclusion......Page 484
Introduction......Page 486
Background......Page 487
DPLL($\Gamma$)......Page 488
Soundness and Completeness......Page 492
Contraction Inferences......Page 493
System Architecture......Page 495
Evaluation......Page 498
Related Work......Page 499
Conclusion......Page 500
Introduction......Page 502
The TPTP Language......Page 503
Higher-Order Logic......Page 504
The THF0 Language......Page 505
Type Checking THF0......Page 508
TPTP Resources......Page 512
Conclusion......Page 513
BNF for THF0......Page 515
Introduction......Page 518
Linear Logic......Page 519
Encoding Object-Logic Formulas, Sequents, and Inference Rules......Page 520
A Focusing Proof System for Linear Logic......Page 521
Sequent Calculus......Page 522
Natural Deduction......Page 524
Natural Deduction with General Elimination Rules......Page 526
Free Deduction......Page 527
System KE......Page 528
Smullyan's Analytic Cut System......Page 529
Related Work......Page 530
Conclusions and Further Remarks......Page 531
Introduction......Page 534
Preliminaries......Page 536
Tree Automata Completion......Page 537
Formalization of Term Rewriting Systems......Page 539
Formalization of Tree Automata......Page 540
An Optimized Inclusion Checker......Page 541
Formalization of Closure by Rewriting......Page 544
Benchmarks......Page 546
Conclusion and Further Research......Page 547
Introduction......Page 550
Preliminaries......Page 553
Term Generation......Page 556
Inference System......Page 557
Simplification Rules for Constructors......Page 558
Induction Inference Rules......Page 559
Soundness and Completeness......Page 561
Handling Partial Specifications......Page 563
Conclusion......Page 564