Jay Thakkar


a bit about me:

I am a final year M.Sc. student, working with Dr. Aditya Kanade. I work in the Software Engineering and Analysis Lab. My research interests include Formal Modeling and Verification, Model Checking, Software Verification, Automata Theory and Complexity. I did my B.Tech in Computer Science and Engineering from Nirma University in 2010.

I was born and brought up in Ahmedabad, Gujarat. Hobby-wise, I am a sports enthusiast. Tennis, cycling, running, bridge (a mind-game of cards) and occasional cricket make up my current sporting activities. In terms of ideologies, this is what I strongly believe in: Living well by letting live.

My Research Work

Transducer-based Algorithmic Verification of Retransmission Protocols

  • In this work, we present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We term these protocols retransmission protocols as they achieve reliable communication through repeated retransmission of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively.

  • We propose models for retransmission protocols as transducers operating on bit strings. Streaming string transducers provide a natural way for modeling these protocols and formalizing correctness requirements. We present case studies involving TinyOS serial communication and HDLC retransmission protocols.

  • Publication: Jay Thakkar, Aditya Kanade,and Rajeev Alur. Transducer-based algorithmic verification of retransmission protocols over noisy channels, IFIP Joint Conference on Formal Techniques for Distributed Systems (33rd FORTE/15th FMOODS), 2013.

  • Won the first runner-up prize at IBM ICARE for the poster on "Transducer Models of Sliding Window ARQ Protocols for Noisy Channels".(.PDF) Poster: (.PDF) (.TEX)

  • Presented a poster on "Transducer Models of Retransmission Protocols for Noisy Channels" at Anniversary Symposium of Robert Bosch Center for Cyber Physical Systems. (.PPT)


  • Indian Institute of Science, Bangalore, India
    M.Sc. (Engg.) , Computer Science (GPA: 6.3 / 8.0)

  • Nirma University, Ahmedabad, India
    B.Tech, Computer Science and Engineering, August 2010 (GPA: 8.3 / 10.0)

  • St. Xavier’s High School, Loyola Hall, Ahmedabad, India
    HSC, GSHSEB, 2006 (AGGREGATE: 87.40%)

  • St. Xavier’s High School, Loyola Hall, Ahmedabad, India
    SSC, GSHSEB, 2004 (AGGREGATE: 87.57%)
  • Teaching Assistant
    E0 223: Automated Verification (January 2012 to May 2012)

  • Null Dereference Analysis of Java Programs
    Implemented an intra-procedural data-flow analysis for detecting null dereference bugs in Java programs using Soot analysis framework.

  • Identification of Agricultural Land from Satellite Images
    Data mining concepts like decision tree are used along with image segmentation concepts to distinguish agricultural land area from other areas in a satellite image.

  • OwnyIT - Own your IT assets
    OwnyIT, own your IT assets, is a simple to use, scalable system to address IT infrastructure management needs of small, medium and large organizations. It uses active agents and remote servers to monitor, manage and control the IT networks. It includes various modules like inventory management, power management, application control and monitoring and change management.
  • Publications:
    • “Transducer Models of Sliding Window ARQ Protocols for Noisy Channels”- Appeared in IBM I-CARE 2012, and won the ’Best Poster: First Runner Up’ prize.
    • “C4:5 Based Approach for Identification of Agricultural Land from Satellite Images”. In the proceedings of International Conference on Emerging Trends in Computer Science, Communication and Information Technology (CSCIT-2010), January, 2010.
  • Secured All India Rank 366 in Graduate Aptitude Test in Engineering (GATE-2010) in Computer Science among over 1 lakh applicants with a percentile score of 99.65%.
  • Student coordinator:
    • Perspective Seminar 2012
    • CSA Open Day 2012
    • CSA Undergraduate Summer School

My Courses

  • Automata Theory and Computability
  • Program Analysis and Verification
  • Automated Verification
  • Design and Analysis of Algorithms
  • Topics in Verification


  • C
  • C++
  • OCaml