Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Formal Methods and Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Formal Methods and Coq


chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Formal Methods and Coq
  • Date: Wed, 17 Mar 2004 18:54:02 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, 17 Mar 2004 17:49:56 +0100
"Joseph N. Ruskiewicz" 
<joseph.ruskiewicz AT inf.ethz.ch>
 wrote:

>    The approach that I will be taking will be from the B side and not 
> the C/Java side.
> 
>     So, taking a formal method and then generating the proofs into Coq 
> for proving.

Hi,

You mean you want to somehow use Coq to prove the proof obligations
generated by B (or another specif system)? I am not sure Why will be
directly helpful to you as it takes *programs* as input instead of
specifications. 

A possible approach would be a translation from B specifs to axiomatically
defined coq functions (that may ultimately be implemented (and proved
correct) at the last refinement step). Exciting!

Cheers,

Pierre




Archive powered by MhonArc 2.6.16.

Top of Page