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 as my supervisor. I completed my masters from Chennai Mathematical Institute in 2021. I enjoy reading about formal methods and their applications.
  • I am at IMDEA Software Institute, Madrid visiting Prof. Alessio Mansutti from March to July 2024
  • I was at Amazon as an Applied Science Intern during the summer of 2023
  • I was at TU Wien visiting Prof. Laura Kovacs from February to May 2023


Interests
I am broadly interested in formal verification. Click one of the following to know more about my 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)

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
FMCAD'24 S. Hitarth, Cayden Codel, Hanna Lachnitt, Bruno Dutertre Extending DRAT to SMT NA
STACS'24 S. Hitarth, George Kenison, Laura Kovács, Anton Varonka Linear Loop Synthesis for Quadratic Invariants
OOPSLA'23 Z. Cai, S. Farokhnia, A. Goharshady, S. Hitarth Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts
OOPSLA'23 A. Goharshady, S. Hitarth, F. Mohammadi, H. Motwani Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs
CCS'22 T. Baluta, S. Shen, S. Hitarth, P. Saxena, S. Tople Membership Inference Attacks and Generalization: A Causal Perspective
Nowhere 2021 S. Hitarth, M. Praveen Window Expressions for Stream Data Processing
Master Thesis 2021 S. Hitarth On the relation between the classes of Weighted Automata and Cost Register Automata

Conference, Workshop, and Summer Schools
When What Where
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