viper-admin

Choice of footprint of magic wand is inconsistent with ECOOP15 paper

1

> Created by bitbucket user **abdelzaher** on 2018-05-22 20:34 Here in this example the permission acc(y.f) is transferred from the current state. In the case where x == y this...

Example (functions + sequences) with a potential matching loop

5

> Created by **@mschwerhoff** on 2016-01-14 13:59 > Last updated on 2019-08-28 10:05 Attached file `arraylist-quantified-permissions_LOOP.sil` appears to have a matching loop, when it is simplified by removing function `content`...

> Created by **@mschwerhoff** on 2019-12-28 17:22 Voila \(and potentially other frontends\) regularly needs to havoc _all_ resources of a specific kind, e.g. _all_ instances of a predicate `P`. This...

Silicon's verification never ends in some Viper tutorial's examples

4

> Created by **@fabiopakk** on 2019-01-18 15:45 > Last updated on 2019-08-29 09:46 Silicon doesn&~~~~;t terminate \(in reasonable time\) for the examples listed below. It seems that Z3 gets &;stuck&;....

Poor and/or fluctuating performance of two programs using magic wands

3

> Created by **@mschwerhoff** on 2017-03-06 15:11 > Last updated on 2019-08-28 10:21 Attached file `BinomialHeap-SlowWand.sil` takes surprisingly long to verify, but doesn&~~~~;t use quantifiers, sequences, or any other &;known&;...

block_array examples exhibit unstable Z3 performance - potentially related to non-linear arithmetic

1

> Created by **@mschwerhoff** on 2017-02-01 13:29 > Last updated on 2019-08-28 10:06 The examples `quantifiedpredicates\issues\block_array.sil` and `quantifiedpredicates\examples\two_blocks_array.sil` exhibit unstable Z3 performance: sometimes, Z3 doesn't terminate, but with very little...

Examples testHistogram.sil and testHistogramFull.sil don't terminate

6

> Created by **@mschwerhoff** on 2015-06-08 10:07 > Last updated on 2019-08-28 09:52 After Silicon-QP commit , `quantifiedpermissions\third_party\testHistogram.sil` and `quantifiedpermissions\third_party\testHistogramFull.sil` no longer terminate (in reasonable time). It is not clear...

Silicon and Carbon fail on AVLTree example translated by Chalice2Sil

2

> Created by bitbucket user **juhaszu** on 2014-05-26 13:47 > Last updated on 2019-08-28 09:42 All failures are for calling a method wihtin a constraining block, where the precondition quantifies...

Clarify the semantics of AST-to-CFG transformation and how to handle irreducible CFGs

11

> Created by **@gauravpartha** on 2019-07-15 08:14 > Last updated on 2019-07-23 13:05 Consider the following example ``` method minimal() { goto loopHead while(true) { label loopHead invariant true assert...

Sequence-related incompletenesses

3

> Created by **@alexanderjsummers** on 2019-05-16 12:22 > Last updated on 2019-05-16 13:37 This is a catch-all issue for observable incompletenesses in the sequence axiomatisation. Since I started upgrading the...