silver
silver copied to clipboard
viperproject
Definition of the Viper intermediate verification language.
The following domain definition is from the 2vyper project [here](https://github.com/viperproject/2vyper/blob/master/src/twovyper/resources/struct.vpr). $Struct defines a domain giving a unique identifier to every element of a struct, and $StructOps defines a domain for...
> Created by **@fpoli** on 2018-08-15 15:29 > Last updated on 2018-08-15 15:35 Why there is no `folding ... in ...` expression? * It's the dual of `unfolding`, which exists;...
Gobra frequently generates permission amounts like ``1 / 4000 / 2`` for SCION code by @jcp19. These are intended to be a fractional permission ``1/4000`` divided by two, i.e., the...
Viper would benefit from having some additional built-in types. For example, lots of Viper examples (e.g. in the tutorial) abstract list data structures on the heap to Viper's pure sequences....
If one wants to create a simple generic domain to represent an option type, one could use this (simplified) example: ``` domain Option[T] { function none_val(): Option[T] function some_of(x: T):...
The [Scalastyle](http://www.scalastyle.org/) linter complains about missing `hashCode` definitions in Silver. I'm not sure if we did that intentionally but it seems worth double-checking, adding a comment to Silver if there...
Impure expressions are typically not allowed on the LHS of an implication, except in an `assume` : ``` field val: Int method foo(r: Ref) requires acc(r.val) ==> true ensures acc(r.val)...
If one tries to verify the following Viper program: ```viper function offset(start: Ref, index: Int): Ref method test(start: Ref, l: Int) ensures forall ii: Int :: 0 offset(start, 0 +...
It is currently unclear how permission introspection should behave inside the body of unfolding expressions, i.e., what the permission mask should be when evaluating the body. We have had some...
With Z3 it's possible to [declare special relations](https://microsoft.github.io/z3guide/docs/theories/Special%20Relations) such as partial order, linear order, etc. The documentation explains that the decision procedure is efficient and avoids the quadratic number of...
Metadata
Owner
Metadata
Definition of the Viper intermediate verification language.