Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Incremental verification

  • Subject: [Frama-c-discuss] Incremental verification
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 06 Oct 2010 17:54:58 +0200
  • In-reply-to: <1758740548.463372.1286194402501.JavaMail.root@zmbs1.inria.fr>
  • References: <1758740548.463372.1286194402501.JavaMail.root@zmbs1.inria.fr>
On 10/04/2010 02:13 PM, Boris Hollas wrote:
> Hi,
>
> this is a proposal for a feature: When writing and verifying code, you
> typically do the following:
>
>    repeat
>      change some lines in your code or specification
>      run Jessie
>    until verified
>
> I'd like to considerably reduce the time needed for Jessie in this loop.
> The Visual Studio plugin for Spec# has a feature that lets the verifier
> run each time the content of the buffer has been changed. This gives
> immediate feedback and greatly improves productivity because you can
> very quickly narrow down the reason why the code doesn't verify. Is a
> similar feature possible for Frama-C/Jessie? For example, Frama-C may
> watch the source file. Each time a change is detected, Jessie is run
> again, but only for the parts that changed. Thus, contracts for
> unaltered functions that had previously been verified don't have to be
> verified again, which will save a lot of time. Caching of proofs and
> failed proofs may also speed up Jessie.
>    

Hi,

I know the Spec# demo within Visual Studio: impressive and very 
professional advertisement :-)

<begin advertisement>

Indeed the next Why/Jessie version, scheduled for december, will have 
support
for some if these: cache of already proved goals, and better parallel 
calls of external provers.
Hopefully it will allow to focus on the changes quickly. But this will 
not run at every file save, because
it might take too long time.

This will be in a newly designed GUI. It will also offer the possibility 
to call an interactive
prover like Coq on individual goals (a long awaited feature...)

<end of advertisement>

- Claude







-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |