Predictable Verification using Intrinsic Definitions
<|reference_start|>Predictable Verification using Intrinsic Definitions: 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 that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.<|reference_end|>
@article{murali2024predictable,
    title={Predictable Verification using Intrinsic Definitions},
    author={Adithya Murali, Cody Rivera, P. Madhusudan},
    journal={arXiv preprint arXiv:2404.04515},
    year={2024},
    doi={10.1145/3656450},
    archivePrefix={arXiv},
    eprint={2404.04515},
    primaryClass={cs.PL cs.LO}
}