Undergraduate Research & Scholarships

Amar Shah L&S Math & Physical Sciences

An Eager SMT Solver for Queries Over Algebraic Data Types

Software verification is the process of mathematically proving that a software system does what it is intended to do, without any bugs. To do these kinds of proofs, software verification engines generate logical queries and use computational tools called satisfiability modulo theory (SMT) solvers to answer these queries.

We are building a new SMT solver that can handle queries containing Algebraic Data Types (ADTs). ADTs are a programming construct classically found in functional programming languages but are increasingly found in all kinds of modern languages (including Rust and even Python!). ADTs are a convenient generalization of structures like lists, and binary trees. If you write a program that contains any of these structures, you could use our SMT solver to help verify your code.

Message To Sponsor

Thank you so much for your support of my project. This helps me continue my research this summer. This is in turn will help me go to graduate school to pursue my dream of building formally verifiable software.
Major: Mathematics & Computer Science
Mentor: Sanjit A Seshia
Sponsor: Anselm MPS Fund
Back to Listings
Back to Donor Reports