Atanu Kundu

About

Hi!, I am a final-year Ph.D. student at the School of Mathematical and Computational Sciences in IACS Kolkata, being advised by Dr. Rajarshi Ray. I am working in the field of falsification of Cyber-Physical Systems, developing tools for obtaining counterexamples from CPS, exploring machine learning techniques, and applying them to the falsification of CPS.

Senior Research Fellow

@SMCS, IACS Kolkata

I originate from a quaint Indian village located in the Bankura region of West Bengal. I reside with my parents in Kolkata, famously known as the "City of Joy", where I am earnestly engaged in the scholarly endeavor of acquiring a Ph.D. My early life unfolded within a diverse family setup. It taught me valuable lessons about respecting seniors, nurturing relationships with colleagues, and motivating youngers regardless of the situation. I am convinced that these foundations have been instrumental in cultivating my distinct sense for managerial capacities.

Research Interest

Hybrid systems attained a strong reception from industry and academia for developing smart devices and applications. Nowadays, such systems are everywhere, from smart buildings to medical devices to autonomous cars. My current research interest is the verification of compositional hybrid systems, where several hybrid system components are connected to form a complex hybrid system.

Hybrid Systems

Hybrid systems consist of both continuous and discrete dynamics behavior, i.e., systems that are hybrid in nature are called hybrid systems or sometimes called cyber-physical systems. Such systems can arise when a digital controller interacts with the physical world via cameras and sensors, like the controller of an autonomous car, robots, etc. Nowadays, such systems are developing rapidly and showing immense use everywhere, from medical devices to automobiles. Building a reliable hybrid system is different from developing traditional systems. The latter is of no direct help to build the former due to its leading characteristics: real-time computation, safety-criticality, etc.

Formal Verifications

Formal verification is a technique used to prove or disprove the correctness of a system or program using mathematical methods. It involves defining formal specifications of the system's behavior and using formal methods such as theorem proving, model checking, and static analysis to verify if the system satisfies the specifications. Formal verification can help detect and eliminate errors, improve system reliability and safety, and reduce the cost of testing and debugging. It is widely used in safety-critical systems such as avionics, automotive, and medical devices. However, formal verification can be computationally expensive and requires expertise in formal methods and software engineering.

Bounded Model Checking

Bounded model checking (BMC) is a technique used in formal verification to verify whether a system satisfies a given property. It involves constructing a mathematical model of the system and encoding the property specification into logic formulas. Then check if the property holds for all possible execution paths of the system up to a certain length or "bound". If the property holds for all bounded execution paths, then it is concluded that the system satisfies the property for all possible executions. BMC has several advantages over other verification techniques, such as being more efficient than exhaustive model checking and being able to handle complex properties.

Machine Learning

Machine learning is a subfield of artificial intelligence that focuses on developing algorithms and models that enable computers to learn from data and improve their performance on a task without being explicitly programmed. Machine learning involves identifying patterns in data through statistical analysis and then using those patterns to make predictions or decisions. Nowadays, it has become one of the hottest research areas because it has the capability to predict or approximate the actual behavior of the system in every field of research.

Skills

C 90%
C++ 90%
SMT-LIB2 80%
Python 80%
MATLAB 80%

I work on the research and development team for the tools that are used to verify/falsify the hybrid systems. The tools are:

  • SAT-Reach
  • NNFal
  • XSpeed

    • Resume

    For more details,

    Sumary

    Atanu Kundu

    • SRF, IACS Kolkata
    • mcsak2346@iacs.res.in

    Education

    Doctor of Philosophy in Computer Science

    2020 - 2025

    Indian Association for the Cultivation of Science, Kolkata, India.

    Developing algorithms and tools for detecting unsafe behavior in CPS.

    Studied two courses as a Ph.D coursework:

    • Advanced Machine Learning
    • Big Data Analytics

    Master of Science in Computer Science

    2016 - 2018

    Visva Bharati, Shantiniketan, India

    Studied several core and advanced courses such as Algorithms, Operating Systems, Automata, DBMS, AI, Image Processing, Approximation Algorithms, etc.

    Projects

    • SatG: A Path Planner for Robots in a 2D Grid using SAT-solving. Under the supervision of Dr. Ansuman Banerjee, ISI Kolkata, India.
    • Building Neural Network Models (FNN) of the Standard CPS such as Hybrid Automata and Simulink Models. Under the supervision of Dr. Rajarshi Ray, IACS Kolkata, India.

    Professional Experience

    Publications

    • A. Kundu, S. Gon, and R. Ray, “Data-driven falsification of cyber-physical systems,” In Proceedings of the 17th Innovations in Software Engineering Conference, ISEC ’24, New York, NY, USA, 2024. Association for Computing Machinery. isbn: 9798400717673. doi: 10.1145/3641399.3641401.[video]
    • A. Kundu, S. Das, and R. Ray, “Sat-reach: A bounded model checker for affine hybrid systems,” ACM Trans. Embed. Comput. Syst., vol. 22, no. 2, Jan. 2023, issn: 1539-9087. doi: 10.1145/3567425.
    • C. Menghi, P. Arcaini, A. Kundu, et al., “Arch-comp23 category report: Falsification,” in Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), G. Frehse and M. Althoff, Eds., ser. EPiC Series in Computing, vol. 96, EasyChair, 2023, pp. 151–169. doi: 10.29007/6nqs.
    • L. Bu, G. Frehse, A. Kundu >, R. Ray, Y. Shi, and E. Zaffanella, “Arch-comp22 category report: Hybrid systems with piecewise constant dynamics and bounded model checking,” in Proceedings of 9th International Workshop on Applied, vol. 90, 2022, pp. 44–57. doi: 10.29007/lnzf
    • L. Bu, A. Kundu , R. Ray, and Y. Shi“Arch-comp24 category report: Hybrid systems with piecewise constant dynamics and bounded model checking,” in Proceedings of 11th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH24), G. Frehse and M. Althoff, Eds., ser. EPiC Series in Computing, vol. 103, 2024, pp. 1–14. doi: 10.29007/nv67
    • C. Menghi, T. Khandait, A. Kundu, et al., “Arch-comp24 category report: Falsification,” in Proceedings of 11th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH24), G. Frehse and M. Althoff, Eds., ser. EPiC Series in Computing, vol. 103, EasyChair, 2024, pp. 122–144. doi: 10.29007/hgfv.

    Talk

    Data-driven Falsification of Cyber-Physical Systems.

    17th Innovations in Software Engineering Conference (ISEC) 2024

    IIIT Bangalore

    SAT-Reach: A Bounded Model Checker for Affine Hybrid Systems.

    Formal Method Update Meeting 2022

    IIT Delhi

    A Framework for Detecting Unsafe Behaviour in Cyber-Physical Systems.

    Tech Symposium on Computing Trends 2023

    Thales India & University of Calcutta

    Contact

    Looking for more information, please feel free to get in touch with me. I'm always eager to connect with enthusiastic individuals.

    Location:

    Kolkata, India

    Loading
    Your message has been sent. Thank you!