S Hitarth
Postdoctoral Researcher
Max Planck Institute for Software Systems
CV    

Hello,
I am currently a postdoctoral researcher at the Max Planck Institute for Software Systems, working with Joël Ouaknine. I received my PhD from HKUST in January 2026, supervised by Amir Goharshady and Fangzhen Lin. Before that, I completed my master's degree in 2021 from Chennai Mathematical Institute. I enjoy reading about topics in theoretical computer science.


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

Arithmetic theories are first-order logical theories where the variables range over numerical domains such as integers and reals, and the predicates are algebraic expressions. Examples include Nonlinear Real Arithmetic (NRA) and Linear-Exponential Integer Arithmetic (LEIA). These theories are often used to encode constraints in program verification, synthesis, and optimization problems.

Work
We show that Integer linear-exponential programs (ILEP), that extend integer linear programs with an exponential function and a remainder function, admit a concise representation for their optimal value, if it exists. S Hitarth, Alessio Mansutti, Guruprerana Shabadi, Optimization modulo Integer Linear-Exponential Programs (SODA'26)

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 situation 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 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) Ofec Israel, Yoni Zohar, Andrew Reynolds, S Hitarth, Bruno Dutertre, Clark Barrett, Cesare Tinelli, Checking Regular Expressions in Cvc5 Proofs (IJCAR'26)

Automata are abstract models of computation 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 the next state. The most powerful automaton is the Turing machine.


The Turing machine is such a powerful model of computation that nothing non-trivial can be decided about such machines (Rice Theorem). For example, we cannot decide whether a given Turing machine will terminate its execution on a given input, or will just keep running forever!
Therefore, we usually restrict ourselves to weaker models of computation such as Weighted Automata, Cost Register Automata, 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 the 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
IJCAR'26 Ofec Israel, Yoni Zohar, Andrew Reynolds, S Hitarth, Bruno Dutertre, Clark Barrett, Cesare Tinelli Checking Regular Expressions in Cvc5 Proofs
JSA'26 Xuran Cai, Amir Kafshdar Goharshady, S Hitarth, Chun Kit Lam Series–parallel-loop Decompositions of Control-flow Graphs
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
PhD Thesis 2025 S Hitarth Synthesis, Proofs, and Optimization in Arithmetic Theories
Master's Thesis 2021 S Hitarth On the relation between the classes of Weighted Automata and Cost Register Automata

Conferences etc.
When What Where
June 2026 SAMSA'26 Warsaw, Poland
January 2026 SODA'26 Vancouver, Canada
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