Pankaj P. Chauhan

The current version of this curriculum vitae is available as
http://www-2.cs.cmu.edu/~pchauhan/resume/resume.txt

Objective:
Not looking for a job.

Biographical Information:
Citizenship:	India
Visa Status:    H1-B
Email:		p-c-h-a-u-h-a-n-+-@-c-s-.-c-m-u-.-e-d-u (without dashes)
Web:		http://www-2.cs.cmu.edu/~pchauhan

Availability: Not looking for a job.

Research Interests:
  Formal Verification, specifically Model Checking
  Computer Architecture/Hardware design

Education:
  Ph.D. in Computer Science (Work done Oct 2004, defended April 2007)
  M.S. in Computer Science (December 2001)
  Computer Science Department
  Carnegie Mellon University
  Pittsburgh, PA
  Research Advisor: Dr. Edmund Clarke
  Member of Model Checking group at CMU.

  Thesis Title: Verification of Large Industrial Circuits Using
    SAT Based Reparameterization and Automated
    Abstraction-Refinement 

  Research Interests: I am interested in applying formal
    verification techniques to large scale systems.  I'm
    specifically interested in techniques to increase the capacity
    of Formal Verification engines using SAT procedures to improve
    automatic abstraction/refinement, image computation, and
    symbolic simulation with reparameterization.  Symbolic
    simulation with SAT based reparameterization increases the
    capacity of property verification by bounded model checking.
    I'm also interested in all solutions SAT engines, which are
    critical for the performance of various algorithms.

  Relevant Courses: Formal Verification of Reactive and
    Concurrent Systems, Computer Systems, Parallel Computing,
    Advanced Networking, Algorithms, Type Systems, Advanced
    AI, Math Logic, Superscalar Processor Design, Performance
    Modeling, Prog. Analysis and Abstract Interpretation, Math
    Logics, Applied Logic by Dana Scott, Algorithms in the Real
    World, Hoare Logic

  Bachelor of Technology in Computer Science and Engineering (May 1998)
    Computer Science and Engineering Department
    Indian Institute of Technology, Kharagpur
    Kharagpur, India

    B. Tech. dissertation: Exploiting Direct Isomorphism to
                           Compress ROBDDs
    Advisors: Dr. Pallab Dasgupta and Dr. P. P. Chakraborty
    GPA: 9.5/10
    First position in the B. Tech. Computer Science and Engg. Class
    Second position among about 450 undergraduates at the
      institute
    Relevant Courses: Digital Design and two courses on
      Computer Architecture, VLSI Design, Switching Theory, Automata &
      Formal Languages, Discrete Math, Parallel Computing, Algorithms,
      Control Systems etc.

Professional and Research Experience:
  Oct 04 to Present - Calypto Design Systems, Santa Clara, CA
    Various roles in the formal equivalence checking group.

  May 02 to August 02 - Strategic Cad Labs, Intel, Hillsboro, OR
    Summer Internship with Dr. Jin Yang.
    SAT based automated abstraction refinement for GSTE.	

  May 01 to July 01 - NEC C&C Research Labs, Princeton, NJ
    Summer Internhship with Dr. Arti Gupta and Dr. Pranav Ashar
    Verification of designs of industrial scale, Bounded Model
    Checking algorithms

  May 99 - July 99, Bell Laboratories, Murray Hill, New Jersey.
    Summer Intern.  Worked with Dr. Kurshan on formal specification
    and verification of PCI bus, Lucent Proprietory F-Bus and
    their interfaces.

  Jan 98 - Apr 98, IIT Kharagpur. Design Lab project.
    A compiler for mapping thread-based shared-memory concurrent
    programs to PVM distributed processes.

  Jul 97 - Apr 98, IIT Kharagpur. B.Tech. thesis research on ROBDDs.

  May 97 - Jul 97, DDE-ORG Systems, Vadodara, India. 
    Summer intern. Developed hardware and firmware for
    dedicated Online Betting Terminals for Bangalore racecourse.

  Apart from these, some other interesting projects during my
    B. Tech. include a compiler for C, hardware implementation of
    a 4-bit CPU, hardware/firmware for a real time bank token
    monitoring system, design and implementation of an FSK modem etc.

  Teaching Experience/Communication Skills:
    15-398 Bug Catching: Automated Software Verification, Fall 2001

    15-441 Undergraduate Algorithms, Spring 2000

    CMU CS departmental speaking skills requirement

    Various conferences and talks

Selected Publications:
  P. Chauhan, E. M. Clarke, D. Kroening, A SAT-Based Algorithm for
     Reparameterization in Symbolic Simulation, DAC 2004.

  P. Chauhan, E. M. Clarke, D. Kroening, Using SAT Procedures for
     Reachability Analysis, SRC TECHCON, 2003.

  P. Chauhan, E. M. Clarke, S. Sapra, J. Kukula, H. Veith,
    D. Wang, Automated Abstraction Refinement for Model Checking 
    Large State Spaces using SAT based Conflict Analysis,
    FMCAD 2002, pp. 33-51.

  P. Chauhan, E. M. Clarke, S. Jha, J. Kukula, T. Shiple,
    H. Veith, D. Wang, Non-linear quantification scheduling for
    efficient image computation, ICCAD 2001, pp. 293-298.

  P. Chauhan, E. M. Clarke, S. Jha, J. Kukula, H. Veith,
    D. Wang, Using Combinatorial Optimization Algorithms for
    Efficient Image Computation, CHARME 2001, pp. 293-309.

  R. Bryant, P. Chauhan, E. Clarke, A. Goel, A Theory of
    Consistency for Modular Synchronous Systems, FMCAD
    2000, pp. 486-504.

  P. Chauhan, P. Dasgupta, P.P. Chakraborty, Exploiting Graph
    Isomorphism for BDD Compaction and Faster Simulation,
    Proceedings of the International VLSI conference, '99, Goa,
    India.

  P. Chauhan, E. Clarke, Y. Lu, D. Wang, Verifying IP-Core Based
    System-On-Chip Designs, IEEE International Conference on
    ASIC/SOC, pp. 27-31, September, 1999.

Professional Activities:
  Referee  for CAV '99, IEEE TPDS 2000, CAV '00, CAV'01, FMSD,
    JAR 2002, CAV'03, DAC'04 and other conferences

Awards and Honors:
  CMU Computer Science Departmental Fellowship, 1998-present

  President of India Silver Medal, Indian Institute of
  Technology, Kharagpur for best academic	performance in
  B. Tech. Computer Science and Engineering class, May 1998

  Award for the second best academic performance among 450+
  undergraduate students of IIT Kharagpur, May 1998

  B.P. Poddar Merit Scholarship, July 1997 to April 1998

  Chief Minister's award/gold medal for being the topper among
  50,000+ students in Gujarat State Higher Secondary Board
  Examination June 1993 

  National Merit Scholarship Certificate, June 1993

Skills:
  OSes: 
    Linux, Unix and variants

  Languages: 
    Current: C, C++, SMV, FL, Lex, Yacc, Verilog, Perl
    Past: Nesl, SQL, Fortran 77, MIPS/Alpha/x86 Assembly, Java, ML

  Development:
    Verification using SMV/VIS/Forte (GSTE) systems.

    Logic design and synthesis using Cadence tools

    TTL, programmable logic and microcontroller based logic design

    Development of parallel programs using threads, Nesl, PVM, MPI
    on various supercomputers

    Development of network applications using Berkeley  sockets
    and WinSock Development of distributed applications using
    DCOM/OLE

Human Languages:
  Fluent English, native Marathi speaker and native skills in
  Hindi and Gujarati (Marathi, Hindi and Gujarati are Indian
  languages)

Personal Interests:
  Model Trains in HO scale (when I get job I will regularly invest
  in this hobby), Hindi and Hindustani Classical Music
  (listening and collecting), Flying Indian Kites, Math and puzzle
  solving

References:
  Prof. Edmund Clarke, Computer Science Departent, Carnegie
    Mellon University
  Dr. Aarti Gupta, NEC C&C Research Labs, Princeton, NJ 08817.
  Dr. Jin Yang, Strategic Cad Labs, Intel, Hillsboro, OR.
  Others available upon request