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.

publications

A New Decision Procedure for

Finite Sets and Cardinality Constraints in SMTNew!Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli

(to appear)In Proceedings of IJCAR, 2016.

Deciding Local Theory Extensions via E-matchingCommutativity Condition RefinementEager and Lazy Approaches to Bit-vectorsLiana Hadarean, Kshitij Bansal, Dejan Jovanovic,

Clark Barrett, and Cesare Tinelli

In Proceedings of CAV, 2014.

Model Checking Bounded Multi-Pushdown SystemsStructural Counter AbstractionBeyond Shapes: Lists with Ordered DataKshitij Bansal, Remi Brochenin, Etienne Lozes

In Proceedings of FoSSaCS, 2009.

projects

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

articles

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