cs.nyu.edu/ ~kshitij/

I am a PhD student in the computer science department advised by Clark Barrett and member of the Analysis of Computer Systems group. My research interests span formal verification of hardware and software systems, including concurrent systems; constraint solvers, automated deduction and logic. Email: kshitij@cs.nyu.edu.


Deciding Local Theory Extensions via E-matching New!
Kshitij Bansal, Andrew Reynolds, Tim King,
Clark Barrett, and Thomas Wies
In Proceedings of CAV, 2015.
[Examples], Evaluation [data], [slides].
Commutativity Condition Refinement New!
with Eric Koskinen, Omer Tripp
(EC)2, 2015.
(conference version under submission)
Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Kshitij Bansal, Dejan Jovanovic,
Clark Barrett, and Cesare Tinelli
In Proceedings of CAV, 2014.
Model Checking Bounded Multi-Pushdown Systems
with Stephane Demri
In Proceedings of CSR, 2013.
Techincal report available at [arXiv]. [slides].
Structural Counter Abstraction
with Eric Koskinen, Damien Zufferey, Thomas Wies
In Proceedings of TACAS, 2013.
Evaluation [data]. [slides].
Beyond Shapes: Lists with Ordered Data
with Remi Brochenin, Etienne Lozes
In Proceedings of FoSSaCS, 2009.


A Satisfiability Modulo Theory (SMT) solver.
Automatically generating commutativity conditions from data-structure specifications.


A branching heuristic
An article describing a branching heuristic implemented in CVC4.