M. Subramaniam (Subu)

Assistant Professor

 

 

Brief Vita

 

 I received my undergraduate degree in Computer Science from Birla Institute of Technology and Science (BITS) Pilani, India in 1986. I received my masters and doctorate in Computer Science from SUNY Albany New York in 1997. I have worked in the software and semiconductor and CAD industry for over 10 years. I was a core developer of a production quality retargettable compiler for a high-level language called CHILL for the telecommunication industry. I also worked in the semiconductor industry in California at SGI, FUJITSU and start-up company Redswitch (acquired by Agilent). My work in these companies involved verification and architecting high-end processors, distributed shared memory systems and I/O network adapters involving Infiniband and FibreChannel protocols.

 

Honors and Awards

·         Distinguished Dissertation Award, SUNY Albany.

·         Woody Bledsoe Student Award on Automated Reasoning

·         National Merit Scholar

·         Guest Scientist, Los Alamos Labs.    

 

Research Interests: Verification and validation of industrial-strength hardware and software systems, simulation, VLSI design methodologies, CAD, distributed shared memory systems and protocols, network I/O protocols and language processing.

 

Research Statement: With rising complexity of hardware and software systems verification and validation is fast becoming a major bottleneck in delivering robust systems under stringent time-to-market pressures. I believe that formal verification and validation approaches tightly integrated with development process provide an effective means to address this problem. Automation and scalability are crucial to the success of these approaches in practice. My research activities focus on developing novel verification and validation approaches to address the above two aspects and have lead to successful verification several industrial-strength arithmetic circuits, cache coherence protocols, and emerging network I/O protocols in a push-button manner.

 

Research Projects: (Under Construction)  

  • SAIL: Joint project with University of New Mexico and University of Iowa on building a push-button prover.
  • CHIME: Change Impact Analyses Environment for Distributed Systems
  • AdhopSpec: Joint project with Los Alamos Laboratories on formal specification of Simulators.

 

 

Selected Refereed Publications

 

  1. M. Subramaniam and J. Shi, “Using Dominators to extract Protocol Contexts,” To Appear in Proc. of Third IEEE Intl. Conference on Software Engineering and Formal Methods (SEFM), 2005.
  2. M. Subramaniam,  “Preserving Consistency of Runtime Monitors across Protocol Changes,” In Proc. of Tenth IEEE Intl. Conference on Engineering of Complex Computer Systems (ICECCS), 2005.
  3. M. Subramaniam and P. Conway, “Early Error Detection in Cache Coherence Protocols Using Relational Algebra”, To Appear in Intl. Journal on Concurrency and Practice, 2005.
  4. M. Subramaniam and P. Chundi, “Preserving Consistency and Executability of Protocols Across Updates”, In Proc. of Intl. Conference on Formal Engineering Methods (ICFEM), LNCS 2004.
  5. D. Kapur, J, Giesl, and M. Subramaniam, “Decidable Induction,” in Journal of Symbolic and Applied Mathematics, (RACSAM), 2004.
  6. M. Subramaniam,   “An Approach for Early Error Detection in Industrial Strength Cache Coherence Protocols Using SQL”, in Proc. of IEEE Workshop on Debugging and Testing of Parallel and Distributed Systems”, IPDPS 2003.
  7. Deepak Kapur and M.Subramaniam  “Automatic Generation of Simple Lemmas from Recursive Function Definitions Using Decision Procedures”, Technical Report, August, 2003. lemmagenrep.pdf.
  8. D.Kapur and M. Subramaniam, Using an Induction Theorem Prover for Verifying Arithmetic Circuits, In Journal on Software Tools for Technology Transfer, 3(1), Springer, pp: 32-65, 2000. Abstract
  9. D.Kapur and M.Subramaniam, Extending Decision Procedures with Induction Schemes, In Proc. Of Seventeenth International Conference on Automated Deduction (CADE-17), LNCS 1831, pp: 324 -345, 2000. Compressed Postscript
  10. D. Kapur and M. Subramaniam, Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory, In Journal of Formal Methods in System Design, 13(2), Kluwer, pp: 127-158, 1998. Compressed Postscript
  11. M. Lowry and M. Subramaniam, Abstraction for Analytic Verification of Concurrent Software Systems, In Proc. Of Symposium on Abstraction, Reformulation and Approximation, 1998.
  12. D. Kapur and M. Subramaniam, Mechanizing Reasoning About Large Finite Tables in a Rewrite Based Theorem Prover, In Proc. of Fourth Asian Computing Science Conference (ASIAN-4), LNCS 1538, pp: 22-42, 1998. Abstract
  13. D.Kapur and M. Subramaniam, Mechanizing Verification of Arithmetic Circuits: SRT Division, In Proc. of Seventeenth International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS 1346, pp: 103-122, 1997. Compressed Postscript.
  14. D. Kapur and M. Subramaniam, New Uses of Linear Arithmetic Procedure in Automated Theorem Proving by Induction, In Journal of Automated Reasoning, 16(1-2), Kluwer, pp: 39-78, 1996. Compressed Postscript
  15. D. Kapur and M. Subramaniam, Lemma Discovery in Automated Induction, In proc. of Thirteenth International Conference on Automated Deduction (CADE –13), LNCS 1104, pp: 538-552, 1996. Compressed Postscript
  16. D. Kapur and M. Subramaniam, Mechanically Verifying a Family of Multiplier Circuits, In Proc. of Eighth Conference on Computer Aided Verification (CAV-8), LNCS 1102, pp: 135-146, 1996. Compressed Postscript
  17. D. Kapur and M.Subramaniam, Automating Induction Over Mutually Recursive Functions, In Proc. of Sixth International Symposium on Algebraic Methodology and Software Technology (AMAST-6), LNCS 1101, pp:117-131, 1996. Compressed Postscript
  18. L. Bertossi, J.Pinto, P.Saez, D.Kapur, M.Subramaniam, Automating Proofs of Integrity Constraints in Situation Calculus, In Proc. of Ninth International Symposium on Methodologies for Intelligent Systems, LNCS 1079, pp: 212-222, 1996.
  19. D. Kapur and M. Subramaniam, Automated Reasoning About Parallel Algorithms Using Powerlists, In Proc. of Fifth International Symposium on Algebraic Methodology and Software Technology (AMAST-5), LNCS 936, pp: 416-430, 1995. Compressed Postscript
  20. D. Kapur and M.Subramaniam, Using Linear Arithmetic Procedure for Generating Induction Schemes, In Proc. of Fourteenth International Symposium on Foundations of Software Technology and Theoretical Computer Science (FSTTCS-14), LNCS 880, pp: 438-449, 1994.
  21. S. Kumar, P.Kumar, M.Subramaniam, V. Buzruk Design of Retargettable CHILL family of compilers, in CHILL: CCITT High Level Language,  North-Holland, Elsevier, Amsterdam, NY 1991.