S Hitarth
PhD Candidate
Hong Kong University of Science and Technology
CV    

About me
Hi, I am a PhD candidate at HKUST with Amir Goharshady and Fanghzen Lin as my supervisors. I completed my masters from Chennai Mathematical Institute in 2021. I enjoy reading about formal methods and their applications.


Interests
I am broadly interested in formal verification. Click one of the following to know more about my work/interest in that area.

Specifying what one intends the program to do is much easier than actually implementing the program. Program synthesis involves automatically generating programs in a specific Domain Specific Language (DSL) that satisfies the given logical specifications. The synthesized program is guaranteed to be correct, by construction.

Work
We present an algorithm to synthesize polynomial programs from the given logical specification using tools from Algebraic Geometry.
A. Goharshady, S. Hitarth, F. Mohammadi, H. Motwani, Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs (OOPSLA'23)

The soundness of Satisfiability Modulo Theories (SMT) solvers is critical in many applications. When the input formula is satisfiable, the solver can typically produce a model that can be trivially checked to be valid. However, when the formula is unsatisfiable, the situations becomes more complex. One way to ensure soundness is to have solvers generate proofs that can be independently verified.

Work
We extend the DRAT proof format for SAT to include the theory reasoning. The proof format is compact and fast to generate and check.
S Hitarth, Cayden Codel, Hanna Lachnitt, Bruno Dutertre, Extending DRAT to SMT (FMCAD'24)

Blockchain is cryptographically linked list of records. There are various Blockchain based platforms such as Ethereum, IBM Blockchain, and Hyperledger Fabric.

Smart Contracts are programs (digital contracts) stored on a Blockchain that are executed when certain conditions are met. One of the interesting thing involved in executing a smart contract in Ethereum is the Gas usage, which is like the fee that one needs to pay to Ethereum for executing the smart contract. If one's smart contract needs more gas then they initially promised, then they lose their gas (read money) and the execution is terminated. Therefore, estimating the upper bound on gas usage for a given smart contract has been an active area of research.


Work
The work is on getting better bounds on gas requirement for a wide class of smart contract by over-approximating them as polynomial programs.
Z. Cai, S. Farokhnia, A. Goharshady, S. Hitarth, Asparagus: Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts (OOSPLA'23)

In processing streaming data like that from hospital intensive care units which continuously generate data, the algorithm that process such data are required to make decision and give relevant output based on data in a given window.
Traditional stream processor let the user define window using imperative programming language which lack formalism and rigor.

Work
M. Praveen and I worked on formalizing the specification of windows using Monadic Second Order (MSO) logic and regular expressions.
S. Hitarth, M. Praveen, Window Expressions for Stream Data Processing (Unpublished)

Automatons are abstract models of computations that move through states while reading an input and ultimately either accept or reject the input. At each state, one letter is read from the input, and depending upon the current configuration of the automaton, it moves to next state. The most powerful automata is Turing Machine.


The Turing Machine is so powerful model of computation, that nothing non-trivial can be decided about them (Rice Theorem). For example, we cannot decide whether the given turing machine will terminate its execution on given input, or will just keep running forever!
Therefore, we usually restrict ourselves weaker model of computations such as Weighted Automata, Cost Register Autamata, etc.

Work
My Master's Thesis, advised by Laure Daviaud, was on relating various classes of weighted automata based on ambiguity and various classes of CRA based on number of registers, etc.
S. Hitarth, On the relation between the classes of Weighted Automata and Cost Register Automata (2021)


Publications etc.
Where Who What Evidence
SODA'26 S Hitarth, Alessio Mansutti, Guruprerana Shabadi Optimization modulo Integer Linear-Exponential Programs
SETTA'25 S Hitarth, M. Praveen Window Expressions for Stream Data Processing
ESOP'25 Amir Goharshady, S. Hitarth, Sergei Novozhilov Efficient Synthesis of Tight Polynomial Upper-bounds for Systems of Conditional Polynomial Recurrences
ASPLOS'25 Xuran Cai, Amir Goharshady, S. Hitarth, Chun Kit Lam Faster Register Allocation via Grammatical Decompositions of Control-Flow Graphs
FMCAD'24 S. Hitarth, Cayden Codel, Hanna Lachnitt, Bruno Dutertre Extending DRAT to SMT
STACS'24 S Hitarth, George Kenison, Laura Kovács, Anton Varonka Linear Loop Synthesis for Quadratic Invariants
OOPSLA'23 Zhuo Cai, Soroush Farokhnia, Amir Goharshady, S Hitarth Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts
OOPSLA'23 Amir Goharshady, S Hitarth, Fatemeh Mohammadi, Harshit Jitendra Motwani Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs
CCS'22 Teodora Baluta, Shiqi Shen, S Hitarth, Prateek Saxena, Shruti Tople Membership Inference Attacks and Generalization: A Causal Perspective
Master Thesis 2021 S Hitarth On the relation between the classes of Weighted Automata and Cost Register Automata

Conferences etc.
When What Where
March 2025 ASPLOS'25 Rotterdam, Netherlands
October 2024 FMCAD'24 Prague, Czechia
March 2024 STACS'24 Clermont-Ferrand, France
October 2023 OOPSLA'23 Cascais, Portugal
January 2023 IBM Neuro-Symbolic AI Workshop 2023 Online Workshop
December 2022 Winter School on Algorithms for Graphs and Games - 2022 Indian Institute of Technology, Jodhpur, India
September 2022 AGATES: Introductory School & Workshop University of Warsaw, Warsaw, Poland
August 2022 SAT/SMT/AR/CP Summer School 2022
CAV'22
Mentoring Workshop (FLoC 2022) 		Technion, Haifa, Israel
July 2022 The Algorithmic and Enumerative Combinatorics 2022 TU Wien, Vienna, Austria
July 2022 Swedish Summer School in Computer Science, 2022 KTH, Stockholm, Sweden
January 2021 POPL 2021 (Symposium on Principles of Programming Languages) Virtual Conference
September 2020 Highlights of Logic, Games, and Automata 2020 Virtual Conference