viper-admin

> **@mschwerhoff** commented on 2014-09-15 14:25 Related: - - - - -

> **@mschwerhoff** commented on 2014-10-06 12:36 Here is another example for an incompleteness. Given the predicate predicate P(x: Ref) { acc(x.f) && (x.f != null ==> acc(P(x)) && unfolding acc(P(x))...

> **@mschwerhoff** commented on 2015-11-20 15:21 Another permission incompleteness is due to separate heap chunks and learning aliasing information after exhaling chunks to aliased receivers: ```text field f: Int method...

> **@mschwerhoff** commented on 2017-01-27 11:27 `incomp2.sil` illustrates another incompleteness that is currently not overcome by failure-driven state consolidations because these don't attempt proofs by contradiction. In the example, the...

> **@mschwerhoff** on 2017-01-27 11:27: > * changed `attachment` from `(none)` to `incomp2.sil`

> **@mschwerhoff** commented on 2017-09-23 13:41 Certain instances of this general completeness issue have been resolved as part of robinsierra's bachelor's thesis.

> **@mschwerhoff** commented on 2019-12-13 15:28 Does Carbon, the other Viper verifier, exhibit the same behaviour? If so, please file an issue at the \[Silver repository\]\([https://bitbucket.org/viperproject/silver](https://bitbucket.org/viperproject/silver)\), because both verifiers should...

> **@alexanderjsummers** commented on 2019-12-13 15:31 Unfortunately, I don't think the two verifiers use the same set of axioms at the moment; neither from the same file, nor the actual...

> Bitbucket user **OmerSakar** commented on 2019-12-13 15:36 I have submitted the \(same\) issue on the Carbon project.

> **@mschwerhoff** commented on 2019-12-13 15:52 Thank you, and yes, please create a Silver issue whose description merely links to the Silicon and Carbon issues.