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.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Rivera, Cody Jackson

Contributors dc:contributor

• Parthasarathy, Madhusudan

• Software Verification
• Automated Reasoning
• Predictable Verification
• Intrinsic Definitions
• Verification Of Linked Data Structures
• Decidability
• Ghost-code Annotations

Statement dc:rights

• Copyright 2024 Cody Rivera

Language dc:language

eng, en

Handle dc:identifier

https://hdl.handle.net/2142/124461

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/124461