About
Hi!, I am a fourth-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
- Birthday: 05 Dec 1994
- Gitlab: https://gitlab.com/Atanukundu
- City: Kolkata, India
- Degree: Ph.D (pursuing)
- Email: atanu94kundu@gmail.com
- Collaboration: Available
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.
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.
Professional Experience
Publications
- Atanu Kundu, Sauvik Gon, and Rajarshi 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.
- Atanu Kundu, Sarthak Das, and Rajarshi 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
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.
Talk
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
Email:
atanu94kundu@gmail.com