Presenter: Siva
Date: 2/8/01
----------
A Taste of Theorem Proving

With the increasing deployment of many real-time and safety critical systems
the critical importance of formal verification is now well accepted.  This talk
will begin with a brief overview of the complementary roles played by
theorem-proving and model-checking in formal verification of systems. We will
then focus on theorem-proving techniques using equational logic and contextual
rewriting which has proved quite successful especially in hardware and protocol
specification and verification.  We will illustrate with examples key concepts
such as termination, confluence and completeness of definitions which help in
building decision procedures and inductive proofs.

========= Some references =========================================
The first two papers are recent surveys of use of theorem proving for
verification. The next two are surveys of Rewrite Systems.
The last one is on proving termination of Associate-Commutative Rewriting.
(online versions of these papers- except 4-- are available from my home page
www.cse.msu.edu/~siva).

1.  John Rushby,
    Theorem proving for verification. In Franck Cassez, editor,
    Modelling and Verification of Parallel Processes: MoVEP 2k, Nantes, France, June 2000.
    Tutorial presented at MoVEP: revised version to be published by Springer LNCS.

2.  Deepak Kapur
    Theorem Proving Support for Hardware Verification. Prelimianry Draft.

3.  N. Dershowitz
    A Taste of Rewriting.  Functional Programming, Concurrency, Simulation and Automated
    Reasoning, Lecture Notes in Computer Science 693, 199-228 (1993)

4.  N. Dershowitz and J.-P. Jouannaud.
    Rewrite Systems, Chap. 6 of Handbook of Theoretical Computer Science B: Formal
    Methods and Semantics, J. van Leeuwen, ed., North-Holland, Amsterdam (1990) 243-320

5. D. Kapur and G. Sivakumar ``Proving Associative-Commutative Termination
       Using RPO-compatible Orderings'' Selected Papers on Automated Deduction
       in Classical and Non-Classical Logics, Lecture Notes in Artificial
       Intelligence 1761, Springer-Verlag, August 1999, pp. 39-61.
_______________________________________________
Sens mailing list  -  Sens@mail.cse.msu.edu
http://www.cse.msu.edu/mailman/listinfo/sens