Papers from PhD work (and its post-PhD extensions)

Program Transformations for Verifying Parameterized Systems (ps, pdf)
Abhik Roychoudhury
Ph.D. Dissertation, State University of New York at Stony Brook, December 2000

• Unfold/fold Transformations for Automated Verification of Parameterized Concurrent Systems (ps),
  Abhik Roychoudhury and C.R. Ramakrishnan
  Invited chapter in a book "Program Development in Computational Logic",
  Editors Maurice Bruynooghe and Kung-Kiu Lau, Springer Verlag, LNCS 3049, 2004, pages 262-291.
  This invited paper also gives a good overview of the formal verification technique based on program transformation developed in my Ph.D. thesis.
  
   
• An Unfold/Fold Tranformation Framework for Definite Logic Programs, (ps)
  Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan and I.V. Ramakrishnan,
  ACM Transactions on Programming Languages and Systems (TOPLAS), 26(3), pages 464-509, May 2004.
  A much expanded version of PPDP 1999 paper. This paper also gives a good overview of the program transformation methods developed in my Ph.D. thesis.
  
   
• Inductively Verifying Invariant Properties of Parameterized Systems, (ps)
  Abhik Roychoudhury and I.V. Ramakrishnan
  Automated Software Engineering Journal, Kluwer Academic Publishers, Volume 11, Issue 2, 2004.
  A much expanded version of CAV 2001 paper.
  
   
• Automated Inductive Verification of Parameterized Protocols, (ps, pdf)
  Abhik Roychoudhury and I.V. Ramakrishnan
  Intl. Conf on Computer Aided Verification (CAV) 2001, LNCS 2102, Springer Verlag.
  
   
• XMC : A Logic Programming based Verification Toolset,
  with C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka et al,
  Intl. Conf on Computer Aided Verification (CAV) 2000, LNCS vol 1855, Springer Verlag.
  
   
• Justifying Proofs using Memo Tables (ps, pdf)
  Abhik Roychoudhury, C.R. Ramakrishnan and I.V. Ramakrishnan
  ACM International Conference on Principles and Practice of Declarative Programming (PPDP) 2000.
  
   
• Verification of Parameterized Systems using Logic Program Transformations (ps, pdf)
  Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan and Scott A. Smolka
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2000, Springer Verlag, LNCS vol 1785.
  • Supplement to the above paper
    Proofs by Program Transformations, (ps, pdf),
    Abhik Roychoudhury, K. Narayan Kumar, C.R, Ramakrishnan and I.V. Ramakrishnan,
    Pre-proceedings of Logic-based Program Synthesis and Transformation (LOPSTR) '99.

   

• Formal MetaTheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems (ps, pdf)
  Amy P. Felty, Douglas J. Howe and Abhik Roychoudhury,
  International Conference on Automated Deduction (CADE) 1999, Springer Verlag, LNCS 1632.
  
   
• A Parameterized Unfold/Fold Transformation Framework for Definite Logic Programs (ps, pdf),
  Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan and I.V. Ramakrishnan,
  International Conference on Principles and Practice of Declarative Programming (PPDP) 1999, Springer Verlag, LNCS 1702.
  
   
• Beyond Tamaki-Sato style Unfold/fold Transformations for normal logic programs, (ps)
  Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan and I.V. Ramakrishnan,
  International Journal on Foundations of Computer Science (IJFCS) Vol 13 No. 3 pages 387-403, 2002.
  Initial version appered in ASIAN 1999, Springer Verlag, LNCS 1742, pages 322-333.
  
   
• Logic Programming and Model Checking (ps, pdf),
  Baoqiu Cui, Yifei Dong, Xiaoqun Du, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan,
  Abhik Roychoudhury, Scott A. Smolka and David S. Warren
  PLILP/ALP 1998, Springer Verlag, LNCS 1490.