Viper [1]}, [2]}
(and its related projects [3]}, [4]}) uses
access annotations (expressed as permission predicates) to explicitly transfer access/mutation
permissions for references between static program names. Like ConSORT,
permissions may be fractionally transferred, allowing temporary shared, immutable
access to a mutable memory cell. However,
while ConSORT automatically infers many ownership transfers, Viper requires extensive
annotations for each transfer.
