Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Tue, 28 Nov 95 15:47:28 PST
From: ctchou@fla.fujitsu.com (Ching-Tsun Chou \(Post_Doctorate\))
Message-Id: <9511282347.AA23134@fla.fujitsu.com>
To: info-hol@cs.byu.edu
Subject: Paper available


The following paper is available via anonymous ftp.
Your comments will be appreciated!

Best regards,
- Ching Tsun


    URL:      ftp://ftp.cs.ucla.edu/pub/chou/por.ps

    TITLE:    Formal Verification of a Partial-Order Reduction Technique
              for Model-Checking

    AUTHORS:  Ching-Tsun Chou & Doron Peled

    ABSTRACT:

        {\em Mechanical theorem proving\/} and {\em model checking\/}
        are the two main methods of formal verification, each with its
        own strengths and weaknesses.  Mechanical theorem proving is
        completely general, but requires intensive human guidance.
        Model checking is automatic, but is applicable to only certain
        types of problems.  Clearly, these two methods should be
        combined so that their strengths and weaknesses complement
        each other.  Prior research in this direction has focused on
        how to decompose a verification problem into parts each of
        which is manageable by one of the two methods.  In this paper
        we explore another possibility: we use mechanical theorem
        proving to formally verify a {\em metatheory\/} of model
        checking.  As a case study, we use the mechanical theorem
        prover HOL to verify the correctness of a {\em partial-order
        reduction\/} technique for cutting down the amount of state
        search performed by model checkers.  We choose this example
        for two reasons.  First, this reduction technique has been
        implemented in the protocol analysis tool SPIN to
        significantly speed up the analysis of many practical
        protocols, hence its correctness has important practical
        consequences.  Second, the correctness arguments involved use
        nontrivial mathematics about sequences, relations,
        Mazurkiewicz traces, deterministic transition systems, and
        their interactions, whose formal versions we hope will become
        the basis of a formal metatheory of many model checking
        algorithms and techniques.  Our formalization led to a
        nontrivial generalization of the original informal theory.  We
        also discuss the lessons, both encouraging and discouraging,
        learned from this exercise.