CS Special Seminar: Hitarth Singh "Don’t trust your code: On writing provably correct programs"

Don’t trust your code: On writing provably correct programs

Hitarth Singh
HKUST
Google Scholar

Abstract: A single bug in critical software can have catastrophic consequences. While testing a program on a few random inputs may provide us some confidence, how can we be sure that our program always behaves as intended? Formal verification answers this challenge with techniques to mathematically analyze a program and prove its correctness for all possible (infinitely many) inputs. Even more ambitiously, we can automatically generate a program that is correct-by-construction through program synthesis. I will discuss my research on polynomial program synthesis and its real-world applications, such as analyzing smart contracts and solving recurrence relations. These techniques rely on Satisfiability Modulo Theory (SMT) solvers—automated reasoning tools that lie at the heart of many formal methods. These solvers, extensively used in industry, can reason about all sorts of problems, from verifying hardware designs to solving polynomial equations, including even logic puzzles. Yet, SMT solvers are complex software that are themselves prone to bugs. I will discuss my work and future directions on making proof generation and validation in SMT solvers scalable and more efficient, enabling us to provably verify their results.

Bio: Hitarth is a 4th-year PhD candidate at HKUST. His research interests are in theoretical computer science, especially formal methods, programming languages, and compiler optimization. His current focus is on making SMT solvers faster and more trustworthy. He has collaborated with the automated reasoning group at AWS on proofs for SMT solvers. The main goal of his research is to develop tools to help write reliable software backed by mathematical guarantees. Recently, he started exploring decision procedures for non-linear variants of integer programming.