Kumar Neeraj Verma

Publications

• Helmut Seidl and Kumar Neeraj Verma.
  Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
  RTA 2009. © Springer-Verlag
• Helmut Seidl and Kumar Neeraj Verma.
  Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. [PDF]
  ACM Transactions on Computational Logic 9 (4), 2008. © 2008 ACM.
• Kumar Neeraj Verma and Jean Goubault-Larrecq.
  Alternating Two-Way AC-Tree Automata. [PDF]
  Information and Computation 205(6):817-869, 2007. © Elsevier
• Helmut Seidl and Kumar Neeraj Verma.
  Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses.
  Program Analysis and Compilation, 2006. © Springer-Verlag
• Kumar Neeraj Verma and Jean Goubault-Larrecq.
  Karp-Miller Trees for a Branching Extension of VASS. [PDF]
  Discrete Mathematics and Theoretical Computer Science 7(1):217-230, 2005.
• Jean Goubault-Larrecq, Muriel Roger and Kumar Neeraj Verma.
  Abstraction and Resolution Modulo AC: How to Verify Diffie-Hellman-like Protocols Automatically. [PDF]
  Journal of Logic and Algebraic Programming 64(2):219-251, 2005. © Elsevier
• Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick.
  On the Complexity of Equational Horn Clauses. [PDF]
  CADE 2005. © Springer-Verlag
• Helmut Seidl and Kumar Neeraj Verma.
  Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. [PDF]
  LPAR 2004. © Springer-Verlag
• Kumar Neeraj Verma.
  Alternation in Equational Tree Automata Modulo XOR. [PDF]
  FSTTCS 2004. © Springer-Verlag
• Kumar Neeraj Verma.
  On Closure under Complementation of Equational Tree Automata for Theories Extending AC. [PDF]
  LPAR 2003. © Springer-Verlag
• Kumar Neeraj Verma.
  Two-Way Equational Tree Automata for AC-Like Theories: Decidability and Closure Properties. [PDF]
  RTA 2003. © Springer-Verlag
• Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, and S. Arun-Kumar.
  Reflecting BDDs in Coq. [PDF]
  ASIAN 2000. © Springer-Verlag

Theses and reports

• Kumar Neeraj Verma.
  Two-Way Equational Tree Automata. [PDF]
  PhD Thesis, ENS Cachan, September 2003.
• Kumar Neeraj Verma.
  Reflecting symbolic model checking in Coq. [PDF]
  Mémoire de DEA, DEA Programmation, Paris, September 2000.
• Kumar Neeraj Verma.
  BDDs in Coq. (Describes a certified garbage collector for BDDs) [PDF]
  BTech project report, IIT Delhi, 2000.
• Kumar Neeraj Verma and Jean Goubault-Larrecq.
  Reflecting BDDs in Coq. [PDF]
  INRIA Research Report RR-3859, France, January 2000.