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.