Predictable Verification using Intrinsic Definitions

Adithya Murali, Cody Rivera, P. Madhusudan

We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show th…