Abstract

It is self-evident that correctness is desirable in computer programs. This project experiments with one approach of ensuring program correctness — formally proving the desired properties of programs by simulating its execution using value placeholders. A new programming language with restricted features is designed and two interpreters for it are implemented. The first performs regular execution on concrete values and the second computes in terms of placeholders to deduce relationships between all possible values and thus proves properties about program state.

Advisor

Musgrave, John

Second Advisor

Guarnera, Drew

Department

Computer Science

Disciplines

Logic and Foundations | Other Computer Engineering | Other Computer Sciences | Programming Languages and Compilers | Software Engineering

Publication Date

2025

Degree Granted

Bachelor of Arts

Document Type

Senior Independent Study Thesis

Share

COinS
 

© Copyright 2025 Eric Liu