Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2000)

Invited Paper: 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 Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {305--306},
    location =   {Santa Barbara, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski