Logic in Computer Science (LICS 2000)

Invited Talk: Some Strategies for Proving Theorems with a Model Checker (at LICS 2000)

Authors: Kenneth L. McMillan

Abstract

Model checking techniques make it possible to verify properties of finite state programs of significant complexity in an automatic way. However, they are limited in scale for complexity reasons, and, of course, limited to finite state models. It is natural, then, to consider using a model checker as a decision procedure within a general-purpose theorem prover. In this way, the general-purpose prover could be used to reduce proof goals to finite-state subgoals of sufficiently small scale to be discharged by the model checker. Thus, in principle we can exploit the advantages of model checking to reduce the manual effort required constructing proofs of complex, infinite state systems.

BibTeX

  @InProceedings{McMillan-SomeStrategiesforPr,
    author = 	 {Kenneth L. McMillan},
    title = 	 {Some Strategies for Proving Theorems with a Model Checker},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {305--206},
    location =   {Santa Barbara, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }