cs.nyu.edu/ ~kshitij/

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


A New Decision Procedure for
Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli
(to appear) In Proceedings of IJCAR, 2016.
Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King,
Clark Barrett, and Thomas Wies
In Proceedings of CAV, 2015.
[Examples], Evaluation [data], [slides].
Commutativity Condition Refinement
Kshitij Bansal, Eric Koskinen, Omer Tripp
(EC)2, 2015.
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
Kshitij Bansal, Stephane Demri
In Proceedings of CSR, 2013.
Techincal report available at [arXiv]. [slides].
Structural Counter Abstraction
Kshitij Bansal, Eric Koskinen, Damien Zufferey, Thomas Wies
In Proceedings of TACAS, 2013.
Evaluation [data]. [slides].
Beyond Shapes: Lists with Ordered Data
Kshitij Bansal, 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.