Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Nelly.Maloisel@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 26/11/99 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                        Vendredi 26 novembre, 10h30

                                -----------
                                Shen Wei Yu
                                -----------

                               INRIA - Sophia

              ===============================================
              Integrating theorem proving with model checking
              ===============================================

 

Interactive theorem proving provides a general approach to modeling and 
verification of both finite-state and infinite-state systems but requires 
significant human efforts to deal with many tedious proofs. On the other hand, 
model-checking is limited to some application domain with small finite-state 
space. A natural thought for this problem is to integrate these two 
approaches. To keep the consistency of the integration and ensure the 
correctness of verification, we suggest to use type theory based theorem 
provers as the platform for the integration and build a model-checker to do 
parts of the verification automatically.

We formalise a verification system of both CCS and an imperative language in 
the proof development system Lego which can be used to verify both 
finite-state and infinite-state problems. Then a model-checker, LegoMC, is 
implemented to generate Lego proof terms for finite-state problems 
automatically. Therefore people can use Lego to verify a general problem with 
some of its finite sub-problems verified by LegoMC. On the other hand, this 
integration extends the power of model-checking to verify more complicated and 
infinite-state models as well. In the meantime, we are implementing a model 
checker for Java card programming language based on Coq. This is an attempt to 
apply this technology to real life programming languages.