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: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Wed, 06 Oct 2010 15:57:08 +0200
  • In-reply-to: <AANLkTi=RA4GN7=WWaq019ttoc7dHF6vnHg8QQsUG80+D@mail.gmail.com>
  • References: <1286194386.7104.190.camel@iti27> <AANLkTi=RA4GN7=WWaq019ttoc7dHF6vnHg8QQsUG80+D@mail.gmail.com>
Hello Pascal,

> All in all, you need at least a rudimentary parser for C+ACSL, but nothing too
> sophisticated: being able to detect changes and to build the call tree
> are enough.

But Frama-C already has a parser for C+ACSL. Maybe it's easier to
augment the existing parser with a feature to detect and forward changes
to the subsequent tools in the chain. In that case, a basis to implement
incremental verification would also be given for the abstract
interpretation plugin and any other verification plugin.

> It should also be possible to do it without using Frama-C and without using
> OCaml as the implementation language.
> 
> Caching automated proof attempts from one run to the next would require
> intervention inside the automated prover(s), though. Do some of them
> already provide
> this kind of feature (of course while preserving determinism of proof attempts:
> success should never depend on the cache's contents)?

I don't know anything about the internals of the provers used by Jessie,
so I don't know if any of them have specific support for caching. But
caching could also be implemented in Jessie if just the proved VCs are
cached. If, for example, you just change something in your precondition,
this should give a considerable speedup. 

I don't know if determinism should be a big issue, maybe a proof takes
longer if the cache is empty. Besides, even without caching the prover
may exhibit different behavior if you rearrange your code or
specification without changing semantics.

BTW, is there support for parallel verification?
-- 
Regards,
Boris