Synthesis and Proofs in Arithmetic Theories

PhD Thesis Proposal Defense


Title: "Synthesis and Proofs in Arithmetic Theories"

by

Mr. Hitarth SINGH


Abstract:

This thesis explores program synthesis and proof generation and validation in 
arithmetic theories. In the first part, we focus on synthesis of polynomial 
programs which are widely applicable in cyber-physical systems, hybrid 
systems, and smart contracts. We introduce novel algorithms for syntax-guided 
synthesis for polynomial programs. We demonstrate the practicality of our 
approach by applying our synthesis technique to estimating gas upper-bound 
for smart contracts and generating tight polynomial upper bounds for 
recurrence systems.

In the second part, we shift our attention to Satisfiability Modulo Theory 
(SMT) solvers that form the backbone of many safety-critical applications in 
formal verification, including the synthesis algorithms of the first part. 
SMT solvers, being bulky software, are prone to bugs, and it is essential to 
ensure their correctness. We propose a new proof format, eDRAT, that extends 
the DRAT proof format for Boolean satisfiability to SMT. eDRAT proofs are 
clausal coarse-grained proofs that distinguish the Boolean and theory 
reasoning of SMT solvers. We present a modular and extensible toolchain, 
Valido, for checking eDRAT proofs. Further, we present formally verified 
theory-specific checkers for two core SMT theories.


Date:                   Monday, 24 March 2025

Time:                   5:00pm - 6:00pm (HKT)

Venue:                  Room 2408
                        Lifts 17/18

Committee Members:      Dr. Amir Goharshady (Supervisor)
                        Prof. Fangzhen Lin (Supervisor)
                        Dr. Sunil Arya (Chairperson)
                        Dr. Dimitris Papadopolous