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.


Automatic Generation of Precise and Useful Commutativity Conditions New!
Kshitij Bansal, Eric Koskinen, Omer Tripp
(to appear) In Proceedings of TACAS, 2018.
[Tool], Evaluation [data].
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli
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].
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.