Welcome to My RESEARCH page

image48

Research Interests

I am interested in Mathematical Logic and Programming Language.  In particular, I am interested in building automated tools and techniques to assist programmers write safe and reliable softwares. My broad research areas are Formal Verification, Program Analysis, Programming Language, Abstract Interpretation, Software Engineering, SAT/SMT solvers, Model Checking, and Hardware/Firmware Co-verification. My PhD dissertation focuses on combining Abstract Interpretation and CDCL-based SAT Solvers for precise and scalable formal verification of finite state systems. My thesis is available at https://ora.ox.ac.uk/objects/uuid:680f0093-0405-4a0b-88dc-c4d7177d840f

Patents

  • Rajdeep Mukherjee, Mitra Purandare, Raphael Polig. “Method for Verifying Hardware/Software Co-designs”, Patent US 20170031806.
  • Rajdeep Mukherjee, Benjamin Chen, Habeeb Farah, Ziyad Hanna. “System, Method and Computer Program For Generating a Formal Verification Model”, US Patent (Under Review).
  • Rajdeep Mukherjee, Benjamin Chen, Habeeb Farah, Ziyad Hanna. “System, Method, and Computer Program Product for Automatically Inferring Case-split Hints in Equivalence Checking of an Electronic Design", US Patent (Under Review).
  • Rajdeep Mukherjee, Benjamin Chen, Habeeb Farah, Ziyad Hanna, Ravi Prakash. "System, Method, and Computer Program Product for Sequential Equivalence Checking in Formal Verification", US Patent (Under Review).

Published Papers

  • Rajdeep Mukherjee, Saurabh Joshi, John O'Leary, Daniel Kroening, Tom Melham. "Hardware/Software Co-verification Using Path-based Symbolic Execution",  20th annual workshop on Microprocessor and SOC Test and Verification", MTV 2019. 
  • Eugene Goldberg, Matthias Gudemann, Daniel Kroening, Rajdeep Mukherjee. “Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions)”, IEEE Design, Automation & Test in Europe Conference, DATE 2018. (Best Paper Award).
  • Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham. “Lifting CDCL to Template-based Abstract Domains for Program Verification”, Automated Technology for Verification and Analysis, ATVA  2017.
  • Rajdeep Mukherjee, Mitra Purandare, Raphael Polig, Daniel Kroening. “Formal Techniques for Effective Co-verification of HW/SW Co-designs”, ACM Design Automation Conference, DAC 2017.
  • Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham. “Equivalence Checking of a Floating-point Unit Against a High-level C Model”,  International Symposium on Formal Methods, FM 2016.
  • Rajdeep Mukherjee. “Word-level Formal Verification Using Abstract Satisfaction”, Doctoral Symposium in Formal Methods, 2016. (Best PhD Dissertation Presentation Award).
  •  Rajdeep Mukherjee, Daniel Kroening, Tom Melham - “Beyond Word-level Hardware Verification”, In ACM SIGDA PhD Forum, DAC, 2016.
  • Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening - “v2c - A Verilog to C Translator”, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016.
  • Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom Melham - “Unbounded Safety Verification for Hardware using Software Analyzers”, IEEE Design, Automation & Test in Europe Conference, DATE 2016.
  •  Rajdeep Mukherjee, Daniel Kroening, Tom Melham - “Hardware Verification using Software Analyzers”, In Proceedings of IEEE Annual Symposium of VLSI, ISVLSI 2015.
  •  Rajdeep Mukherjee, Daniel Kroening, Tom Melham, Mandayam Srivas - “Equivalence Checking using Trace Partitioning”, In Proceedings of IEEE Annual Symposium of VLSI, ISVLSI 2015.
  •  Rajdeep Mukherjee, Priyankar Ghosh, Pallab Dasgupta, Ajit Pal - “Operator Scheduling Revisited : A Multi-Objective Perspective for Fine-Grained DVS Architecture”, In proceedings of the International Conference on Advances in Computing and Information Technology, ACITY 2012.
  • Rajdeep Mukherjee, Priyankar Ghosh, N. Sravan Kumar, Pallab Dasgupta, Ajit Pal - “Multi- Objective Low-power CDFG Scheduling using Fine-Grained DVS Architecture in Distributed Framework”, In Proceedings of International Symposium of Electronic Design, ISED 2012. (Best Paper Award)
  •  Rajdeep Mukherjee, Pallab Dasgupta, Ajit Pal, Subhankar Mukherjee - “Formal Verification of Hardware / Software Power Management Strategies”, In Proceedings of International Con- ference on VLSI Design, VLSID 2013.
  • Rajdeep Mukherjee, Subhankar Mukherjee, Pallab Dasgupta - “ Model Checking Global Power Management Strategies in Software with safety LTL properties”, In Proceedings of Indian Software Engineering Conference, ISEC 2013.
  •  Rajdeep Mukherjee, Priyankar Ghosh, Ajit Pal - “Hotspot Reduction using Fine-grained DVS Architecture at 90 nm Technology”, In Proceedings of Asia-Pacific Conference on Postgraduate Research in Microelectronics & Electronics, PRIMEASIA 2012. (Best Paper Award)
  •  Pallab Dasgupta, Mandayam K. Srivas, Rajdeep Mukherjee - “Formal Hardware/Software Co- Verification of Embedded Power Controllers”, In IEEE Transactions on CAD of Integrated Circuits and Systems, TCAD 2014.
  • Aritra Hazra, Rajdeep Mukherjee, Pallab Dasgupta, Ajit Pal, Kevin Harer, Ansuman Banerjee, and Subhankar Mukherjee - “POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent”, In IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems, TCAD 2013.
  • Rajdeep Mukherjee, Priyankar Ghosh, Pallab Dasgupta, Ajit Pal - “An Integrated Approach for Fine-Grained Power and Temperature Management During High-level Synthesis”, In International Journal of Low Power Electronics, Volume 9, Number 3, JOLPE 2013.
  • Rajdeep Mukherjee, Priyankar Ghosh, Pallab Dasgupta, Ajit Pal - “A Multi-Objective Perspective for Operator Scheduling using Fine-Grained DVS Architectures”, In International Journal of VLSI design & Communication Systems, VLSICS Journal, 2013.

Academic Participation

  • Technical Program Committee member in DAC 2019
  • Technical Program Committee member in FMCAD 2019
  • Peer Reviewer of scientific conferences and Journals: DAC 2019, ACSD 2016, NFM 2016, FESCA 2016, TACAS 2016, CAV 2015, MEMOCODE 2015, ICCD 2015, FMCAD 2015, TACAS 2014, CAV 2014, FMCAD 2014, ICCD 2014, MEMOCODE 2014, VLSID 2014, IJES, IEEE Transaction on VLSI, Journal of Circuits, Systems, and Computers (JCSC).

Invited Talks

  • Talk titled “Taming the Verification Challenge in Safety Critical Systems”, Amazon AWS, 2019, California, USA
  • Talk titled “Formal Techniques for Equivalence Checking and Co-verification”, Cadence Design Systems, May 2018, California, USA
  • Talk titled “Formal Verification of Contract Based Designs in Connected Cars”, Invited Talk at Toyota ITC, June 2017, California, USA.
  • Talk titled “Abstract CDCL for Program Verification”–Invited Talk at University of Texas, June 2017, Austin, USA.
  • Talk titled “Methodology and Abstraction for System-Level HW/SW Co-Verification”– SRC 2017, Austin, USA.
  • Talk titled “Formal Techniques for Effective Co-verification of HW/SW Co-designs”–DAC 2017, Austin, USA.
  • Talk titled “Abstraction Techniques for Effective Verification”– Invited Talk, 2017, Intel HQ, Portland, USA.
  • Talk titled “Word-level Formal Verification Using Abstract Satisfaction”– FM 2016, Cyprus 
  • Talk titled “Learning based Assume Guarantee Reasoning for Hardware/SoftwareCo-verification” - Research Talk 2016, IBM Zurich Research Laboratory, Switzerland
  • Talk titled “v2c - A Verilog to C Translator”- TACAS 2016, Eindhoven, Netherlands
  • Talk titled “Unbounded Safety Verification for Hardware using Software Analyzers”- DATE 2016, Dresden, Germany
  • Talk titled “C-RTL Equivalence Checking of Single-precision and Double-precision Floating-point Arithmetic Unit in ARM Graphic Processing Units, Research Talk 2015, ARM HQ, Cambridge, UK
  • Talk titled “How Efficient are Software Verifiers for Hardwares?”-Poster presentation talk at FMCAD 2015, University of Texas, Austin, USA.
  • Talk titled “Equivalence Checking Using Directed Trace Partitioning”- ISVLSI 2015, Montpellier, France
  • Talk titled “Automatic Trace Partitioning Using Abstract Conflict Driven Clause Learning”- Invited talk at University of Utah, April 2015, Utah, USA
  • Talk titled “Hardware Verification Using Software Analyzers”- Semiconductor Review Corporation Review meeting, April 2015, Salt Lake City, Utah, USA
  • Talk titled “Hardware/Software Co-Verification Via Directed Trace Partitioning”- Semiconductor Review Corporation Review meeting, April 2014, Austin, Texas, USA
  • Lecture titled “Formal Verification using CAD tools and Software Model Checking” - June 2012, Advanced VLSI Summer Course, IIT Kharagpur, India
  • Talk titled “Operator Scheduling Revisited : A Multi-Objective Perspective for Fine-Grained DVS Architecture” - ACITY 2012, Chennai, India
  • Talk titled “Multi-Objective Low-power CDFG Scheduling using Fine-Grained DVS Architecture in Distributed Framework”, ISED 2012, Kolkata, India
  • Talk titled “Formal Verification of Hardware / Software Power Management Strategies”, VLSID 2013, Pune, India
  • Talk titled “Model Checking Global Power Management Strategies in Software with safety LTL properties”, ISEC 2013, New Delhi, India
  • Talk titled “Hotspot Reduction using Fine-grained DVS Architecture at 90 nm Technology”. PRIMEASIA 2012, Hyderabad, India