What is difference between VeriFast and Frama-C?

[Kiwamu Okabe]

Hi all,

I understand VeriFast is similar to VCC, while I read some paper.
However, what is difference between VeriFast and Frama-C?

Frama-C can't maintain concurrency?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Bart Jacobs]

Frama-C is a framework with a large ecosystem of plugins, including a
plugin called Mthread <https://frama-c.com/mthread.html>. Furthermore,
Frama-C is constantly being improved.

One of the plugins is the WP plugin <https://frama-c.com/wp.html>, for
modular annotation-based deductive verification of C programs. It is
probably the plugin that yields a user experience that is most similar
to VeriFast.

The main difference between WP and VeriFast is the way the two tools
deal with pointers.

WP verifies a C function by generating proof obligations (formulae of
classical first-order logic) through a weakest precondition computation,
and asking a theorem prover (such as an SMT solver) to discharge these
proof obligations. The weakest precondition computation deals with C
statements that dereference pointers according to one of the supported
memory models (see the WP Manual
<https://frama-c.com/download/frama-c-wp-manual.pdf>), but the general
idea is that memory is modelled in the proof obligations as a function
from addresses to values.

In contrast, VeriFast verifies a C function by symbolically executing
it, dealing with pointer dereferences using a symbolic representation of
memory in the form of a separating conjunction of so-called heap chunks
(separation logic predicates). It generates proof obligations only when
boolean expressions (which do not talk about memory) are asserted, or to
decide equality of pointers and data values.

As for concurrency: the WP Manual does not mention concurrency. The
manual for ACSL, Frama-C's annotation language
<https://frama-c.com/acsl.html>, also does not mention concurrency, but
it does mention built-in predicates "valid" and "valid_read", which one
might be able to use to prove absence of data races.

VCC is similar to Frama-C in that it generates WP-based proof
obligations and does not use a symbolic heap in the VeriFast/separation
logic sense; it is different from Frama-C in that it has extensive
explicit support for concurrency, including two-state invariants that
enable expressing complex protocols governing state shared between
threads. It also has explicit support for ownership, which VeriFast
expresses through heap chunks, and which WP does not have.

[Kiwamu Okabe]

Hi Bart, thanks for your advanced comment.

On Fri, Sep 23, 2016 at 8:48 PM, Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> Frama-C is a framework with a large ecosystem of plugins, including a plugin
> called Mthread <https://frama-c.com/mthread.html>. Furthermore, Frama-C is
> constantly being improved.

But I see that Mthread is not OSS product...

> One of the plugins is the WP plugin <https://frama-c.com/wp.html>, for
> modular annotation-based deductive verification of C programs. It is
> probably the plugin that yields a user experience that is most similar to
> VeriFast.

Good news... but...

> The main difference between WP and VeriFast is the way the two tools deal
> with pointers.
>
> WP verifies a C function by generating proof obligations (formulae of
> classical first-order logic) through a weakest precondition computation, and
> asking a theorem prover (such as an SMT solver) to discharge these proof
> obligations. The weakest precondition computation deals with C statements
> that dereference pointers according to one of the supported memory models
> (see the WP Manual <https://frama-c.com/download/frama-c-wp-manual.pdf>),
> but the general idea is that memory is modelled in the proof obligations as
> a function from addresses to values.

I think I can only understand this line today. < a function from
addresses to values

> In contrast, VeriFast verifies a C function by symbolically executing it,
> dealing with pointer dereferences using a symbolic representation of memory
> in the form of a separating conjunction of so-called heap chunks (separation
> logic predicates). It generates proof obligations only when boolean
> expressions (which do not talk about memory) are asserted, or to decide
> equality of pointers and data values.

I think I understand it.
By the way, the heap chunks are related to proof of linear logic? I
seem they are very similar.

> As for concurrency: the WP Manual does not mention concurrency. The manual
> for ACSL, Frama-C's annotation language <https://frama-c.com/acsl.html>,
> also does not mention concurrency, but it does mention built-in predicates
> "valid" and "valid_read", which one might be able to use to prove absence of
> data races.

The concurrency is very important function for us. Totally, Frama-C is
not miss match for us.

> VCC is similar to Frama-C in that it generates WP-based proof obligations
> and does not use a symbolic heap in the VeriFast/separation logic sense; it
> is different from Frama-C in that it has extensive explicit support for
> concurrency, including two-state invariants that enable expressing complex
> protocols governing state shared between threads. It also has explicit
> support for ownership, which VeriFast expresses through heap chunks, and
> which WP does not have.

O.K.

Thanks a lot,