Stack Overflow
Stack Overflow

Questions tagged [viper-lang]

Viper is an open-source verification infrastructure, designed to simplify the development of formal, separation-logic-based verifiers for different programming languages.

Viper is an open-source verification infrastructure, designed to simplify the development of formal, separation-logic-based verifiers for different programming languages. It comprises (1) a novel intermediate verification language, also named Viper, (2) automatic, SMT-based verifiers for this language, and (3) example front-end verifiers for languages such as Python, Rust, and Go.

The Viper verification language supports a rich set of expressive specification and verification constructs, as well as a simple object-based programming language. This enables and facilitates the development of verifiers for additional languages: by translating a source language and specifications into Viper, other front-ends can be implemented comparably quickly.

Viper has also been used for developing research verification prototypes, e.g. to verify correctness of C11 weak-memory programs, or fine-grained concurrency programs that use atomic instructions for synchronisation. Moreover, Viper has been used for teaching formal methods at several universities.

6 questions
3
votes
1 answer

Invariant fails but assert before loop verifies

In the following program, the last invariant of the loop fails to verify. But if I put it as an assert before the while loop, the condition verifies. If I add that the field ia does not change, it also verifies. Why is this needed? Shouldn't this be…
bobismijnnaam
  • 1,361
  • 2
  • 10
  • 20
3
votes
1 answer

Expected error or incompleteness with quantified permissions and wildcards?

Consider the following Viper program: field f: Int method g(r: Ref, N: Int) requires forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard) { // Got error: insufficient permission for r.f assert 0 < N ==> acc(r.f, wildcard) } method…
Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
2
votes
1 answer

Does multiplying a wildcard in viper mean anything?

A bug in VerCors generated some silver that looks like: field f: Int method test(n: Int, x: Ref) requires n == 100 requires acc(x.f, wildcard * n) {} Viper seems to accept this, but I don't understand what it would mean, if anything.
Pieter Bos
  • 1,554
  • 1
  • 12
  • 20
2
votes
1 answer

double permission inhale leads to unexpected verifications

I have trouble understanding some behaviour of Viper, which, imho, seems to be a bug. The following code fails to verify due to a lack of permissions for bar.val_int on the assignment. This makes total sense. field val_int: Int method foo() { var…
j_beck
  • 64
  • 1
  • 5
1
vote
1 answer

Cannot assert wildcard permission that was in contract

The following program fails to verify: field f: Int method m(g: Ref, i: Int) requires acc(g.f, i * wildcard) { assert acc(g.f, i * wildcard) } I first stumbled upon this where i was a more complex expression (specifically, an abstract…
bobismijnnaam
  • 1,361
  • 2
  • 10
  • 20
0
votes
1 answer

How to refer in postcondition to a wildcard permission in precondition

How can I declare a method requiring a wildcard permission and returning exactly the same permission. I would like the write something like this: field fd:Int method foo(p:Ref) returns (res:Int) requires acc(p.fd,wildcard) ensures…
rsaill
  • 91
  • 1
  • 7