Arshavir Ter-Gabrielyan
Arshavir Ter-Gabrielyan
Hi, We've been experimenting with using Viper for verifying smart contracts in the Motoko language. I've stumbled upon a strange incompleteness: After a method call, I cannot assert a property...
* Z3 version 4.8.6 - 64 bit * Silicon revision ```bc8c538fed426fb973642ff6427ee0b3b4cd629a``` Jenkins build ```#2419``` (02-Apr-2021) * Related issue: #321 The following code: ```viper field val: Int function snap(g: Set [Ref]):...
Asking Carbon to produce counterexamples for the following program results in a crash: ```silver function hello(x: Int): Int method problematic() { var x: Int assert x == hello(x); } ```...
SilFrontend generates AST nodes with incorrect positions. In particular, the start position of methods is wrong (seems to be the same as their end position for some reason). This is...
In particular, ```TerminationPlugin.mapVerificationResult``` in https://github.com/viperproject/silver/blob/master/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala#L125 performs a non-trivial transformation in the following case: ```viper method foo() { assert false } ```
The termination plugin implicitly creates methods that perform termination checks for functions, e.g., in the following scenario: ```viper import function bar(x: Int): Bool decreases x { bar(x) } ``` Since...
In particular, the method ```PartialVerificationError .withReason```, which is implemented in many case classes all over [src/main/scala/viper/silver/verifier/VerificationError.scala](https://github.com/viperproject/silver/blob/76d209c3ac7a174c34c38877afd656b8540a1fd8/src/main/scala/viper/silver/verifier/VerificationError.scala), needs to properly set the field ```cached```. Otherwise, error transformations use ```withReason``` result in...
Hi, I've noticed that your current `sns_proposal.sh` configuration script is setting `--swap-due-timestamp-seconds` to a relatively small value (`1209600` is two weeks in seconds). https://github.com/open-ic/open-chat/blob/39c99c18f985e25abd10be48c7ee047d1de355db/sns_proposal.sh#L40 However, I think that this parameter...
How to use this fix: 0. Make sure you have the "Viper v4.3.1" extension installed in VS Code, and that it has installed its dependencies (this happen via a prompt...
## Overview We believe that code-level verification would be extremely beneficial to all Web3 projects, particularly high-stake applications like DeFi. Late last year, a few formal verification experts from the...