Sreejith A V / ശ്രീജിത്ത് എ വി

Associate Professor, Department of computer science
F6, Academic building, IIT Goa, Farmagudi, Ponda, Goa-403401


About me

    I am interested in formal methods in computer science, theoretical computer science and applications of machine learning.


Formal methods in computer science

    Probabilistic/weighted pushdown automata: In this work, we look at weighted/probabilistic pushdown automata and its various subclasses. We are interested in questions like equivalence, model checking etc. This is an on-going work with Vincent Penelle and Ph.D student Prince Mathew. DST funds my research through the Matrics grant.

    Formal verification of adaptive control algorithms: The objective of this work is to develop the theory and tools to formally verify control logics that use machine learning algorithms. This is a joint work with Vincent Penelle (University of Bordeaux) and Meenakshi D'Souza (IIIT Bangalore). The project is funded under the CEFIPRA grant. More details about the project can be found here. We are looking for Ph.D students for this project.

    Compiler verification: This is an yet to start joint work with Sudakshina Dutta and our Ph.D student Andleeb Zuhra.

    Temporal logic: Standard linear temporal logic (LTL) and first order logic (FO) over words cannot count (even modulo a number). For example, the language (aa)* is not definable in LTL. In our paper [S.], we showed the equivalence of modulo counting extensions of FO and LTL. We also looked at the satisfiabiity problem over these logics [LS1],[LS2]. This was part of my Ph.D work.

Theoretical computer science

    Linear orderings: From the work of Schutzenberger we understand the relation between first order logic and monadic second order logic over finite words. In our work [CS] and [MS] we looked at the relation between logics such as first order, weak MSO and a few more natural logics over countable linear orderings. These algebraic characterizations (called o-monoids) using equations gives us decidability of these logics. We also look at the block product operation for o-monoids [ASS1] and a Krohn-Rhodes style block product characterization for these logics [ASS2].

    Descriptive complexity: First order logic (using arbitrary arithmetic predicates) over words is expressively equivalent to AC0 circuits. Similarly, modulo counting quantifiers and CC0 circuits are closely related. The expressive equivalence of many of the circuit classes are open. We look at these questions from the perspective of logic. In our paper [KS] we show that these circuit classes if we assume "highly uniform" circuit classes.

Applicatons of machine learning

    River topology analysis: In this work we analyse satellite images and in-situ measurements to estimate properties of rivers like river discharge [GMSSKT]. The work was funded by ministry of earth science. Currently MTech students Anshul Moon and Vaishak are working on this. This is a joint work with Gaurav Kumar (IISER Bhopal)

    Soil moisture estimation: In this work, we estimate the soil moisture from satellite images. This is a joint work with Swati Agarwal (Bits Pilani Goa) and Gaurav Kumar (IISER Bhopal). MTech student Ankita Chand is currently working on this project.

    Biology and computer science: Notes on pooled testing (with Somenath Biswas): [pdf]
    Epidemiology: Notes on SIR model (with Somenath Biswas): [pdf]
    National supermodel for COVID19 - Visualization and Data Analysis (with Somenath, Clint, and MTech students Rajat and Vaibhav):

Publications / Unpublished notes

First-Order logic and its Infinitary Quantifier Extensions over Countable Words with Bharat Adsul and Saptarshi Sarkar, FCT 2021 (pdf, full, abstract)
Coupling threshold theory and satellite image derived channel width to estimate the formative discharge of Himalayan Foreland rivers. with K. Gaurav , F. Métivier , R. Sinha , A. Kumar , and S. K. Tandon, Earth Science Dynamics 2021 (pdf, abstract)
Pooled testing with Somenath Biswas (pdf, abstract)
Notes on Parity games (pdf, abstract)
Undecidability of MSO+“ultimately periodic”, with Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle, LMCS 2020 (pdf, abstract)
Block Product for finite monoids with generalized associativity, with Saptarshi Sarkar, and Bharat Adsul (pdf, abstract)
Block products for algebras over countable words and applications to logic, with Saptarshi Sarkar, and Bharat Adsul, LICS 2019. (pdf, abstract)
Lecture notes: Logic for computer scientists (pdf, abstract)
Two-variable first order logic with counting quantifiers: Complexity Results, with Kamal Lodaya,   DLT 2017. (pdf, abstract)
Two-variable logic over countable linear orderings, with Amaldev ManuelMFCS 2016. (pdf, full, abstract)
Limited Set quantifiers over Countable Linear Orderings, with Thomas Colcombet, ICALP 2015. (pdf, full, abstract)
Counting quantifiers and linear arithmetic on word models, with Kamal Lodaya Asian Logic Conference (ALC), 2014. (pdf)
On lower bounds for multiplicative circuits and linear circuits in noncommutative domains, with V. Arvind and S. Raja,  CSR, 2014. (pdf, abstract)
Non-definability of Languages by Generalized First-order Formulas over (N, +), with Andreas KrebsLICS 2012. (pdf, full, abstract)
Expressive Completeness for LTL With Modulo Counting and Group Quantifiers, Electronic Notes in Theoretical Comp Sci (ENTCS), 2011. (pdf, abstract)
LTL can be more succinct, with Kamal Lodaya ATVA 2010 . (pdf, abstract)


ACM India Honourable Mention 2014 for my PhD thesis Regular quantifiers in Logic


Ph.D. students
  • Prince Mathew - weighted/probabilistic pushdown automata
  • Andleeb Zuhra (co-guiding with Sudakshina Dutta) - compiler verification
Masters students
  • Ankita Chand - soil moisture estimation
  • Divya Mishra - Algorithmic trading
  • Anshul Moon - River topology estimation
  • Vaishak D.A. - River width estimation
  • Vaibhav (completed, co-guide Somenath Biswas) - Epidemiology


CS525: Randomized algorithms, Jan-May 2022, BTech/MTech elective course.
CS524: Advanced data structures and algorithms with C++, Aug-Dec 2021, MTech course.
CS220: Data structures and algorithms , Aug-Dec 2021 video lectures-C/C++ Programming
CS531: High dimensional data science , Jan-May 2021 video lectures
CS220: Data structures and algorithms , Aug-Dec 2020 video lectures-C/C++ Programming, video lectures-Data Structures and algorithms
CS500: Algorithm design lab, Aug-Dec 2020
CS520: Combinatorial optimization , Jan-May 2020
CS113: Data structures and algorithms , July-Dec 2020
CS228: Logic for computer science , July-Dec 2019
CS570: Verification, July-Dec 2019
CS315: Advanced algorithms , Jan-May 2019
CS713: Topics in logic and automata theory, July-Dec 2018
CS228: Logic for computer science , July-Dec 2018
CS101: Computer programming , Summer 2018
CS348: Computer Networks Course , Jan-May 2018
CS 378: Computer Networks Lab Jan-May 2018
Reading Logic with Prince

Interesting links

Department research talks: link

Shannon on Creative thinking
Computer science bibliography collections
Computer science conference timelines
Erdos Number
Live chess tournaments