Jamie Kai

This modifies the axiom used to frame heap-dependent functions and predicates with `Set` arguments based on quantified permissions. The following explanation also exists in #522. We noticed that in the...

Heap-dependent function with QPs generates triggerless axiom

2

While considering performance issues for heap-dependent functions, we found that the following function definition in Viper: ``` field f: Bool function heapFun(refs: Set[Ref]): Map[Ref, Bool] requires (forall ref: Ref ::...

Incompleteness for heap-dependent functions with quantified permissions

3

Hello, I've found an unknown source of incompleteness in Silicon while working with heap-dependent functions that are set-valued (and hence require quantified permissions). The following Viper code will verify in...