Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 12 Jan 95 15:39:40 EST
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9501122039.AA20488@ultrastar.EE.CORNELL.EDU>
To: info-hol@leopard.cs.byu.edu
Subject: Summary of replies: combining theorem proving and state-based 
         approaches


Back in October, I asked for references to research that combined
state-base approaches such as  model-checking with theorem proving.

I actually got very few responses, but a lot of requests to
summarize the information I did get.  Here (finally) is my summary.  
I apologize on the lateness -- some of the information may be
out-of-date by now.

(Note: I have edited the replies.  I hope I have not mis-represented
anyone's work.)

First for published work:

1.  In the proceedings of CAV'93 :

"Combining Modelchecking and Theorem Proving to
                        Verify Parallel Processes"
                        Hardi Hungar
pgs 154-165  
Note:  Combines CTL and Lambda

2. In the proceedings of CAV'93 :

"Verification of a Multiplier: 64 Bits and Beyond"
                 R.P. Kurshan, Leslie Lamport

pgs 166-179
Note:  Combines Cospan and TLP (Based on Lamport's TLA)

Many of the pointers were to unpublished work:

3.  From:  Anna Patterson annap@cs.cs.stanford.edu

>PVS from SRI International has a mu-calculus model checker incorporated in
>with its higher-order interactive theorem prover.

>It is a recent addition, quetions should go to sree@csl.sri.com

4. From: Nancy Day <day@cs.ubc.ca>

>First of all, Scott Hazelhurst (shaze@cs.ubc.ca) is doing work
>on building a theorem-prover on top of Voss (which can be
>thought of as a specialized model checker).

>In my master's thesis, I built a model checker for statecharts
>using the HOL-Voss combination.  My semantic definitions and 
>a higher order function which did the model checking were
>written in HOL and then "translated" to FL (the functional
>language interface of Voss) and executed using FL's BDD support.
>Since then, I've moved on to using PVS because it has built
>in BDD support.  I've almost finished rewriting my semantic
>definitions for statecharts in PVS but I've already run some
>simple model checking functions.  The advantage of continuing
>to work within a theorem prover is that I can prove things
>using the semantic definitions.  For example, I want to look
>at properties of composing statecharts and whether model
>checking results can be composed correspondingly.

@MASTERSTHESIS{day:mscthesis,
        AUTHOR = {Nancy Day},
        TITLE = {A Model Checker for Statecharts},
        SCHOOL = {University of British Columbia},
        YEAR = {1993},
        NOTE = {Department of Computer Science, Technical Report 93-35}}

@TECHREPORT{shaze,
        AUTHOR = {Scott Hazelhurst and Carl-Johan H. Seger},
        TITLE = {A Simple Theorem Prover Based on 
                   Symbolic Trajectory Evaluation and OBDDs},
        NUMBER = {93-41},
        INSTITUTION = {University of British Columbia, 
                      Department of Computer Sience},
        MONTH = {November},
        YEAR = 1993 }

> These are both available via www at http://www.cs.ubc.ca/tr/1993/index 


5.  From: Albert Camilleri <ac@gslxsrv.rose.hp.com>

> Kurshan is working on Cospan, and possible integration with HOL.

> Also at the last CAV (1994), Manna talked about a new tool they are
>developing called STEP (Stanford TEpmoral Prover). Their idea is to
>combine deductive techniques with model checking. Alas, the
>proceedings also had no paper, just an abstract.