Recalling a Witness: Foundations and Applications of Monotonic State

Danel Ahman, Cédric Fournet, Catalin Hritcu +3

We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the…