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.