Beyond Shapes: Lists with Ordered Data. - Kshitij Bansal; Rémi Brochenin; Étienne Lozes (FoSSaCS, 2009)

A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems - Kshitij Bansal; Stéphane Demri (CoRR, 2012)

Model-Checking Bounded Multi-Pushdown Systems. - Kshitij Bansal; Stéphane Demri (CSR, 2013)

Structural Counter Abstraction. - Kshitij Bansal; Eric Koskinen; Thomas Wies; Damien Zufferey (TACAS, 2013)

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. - Liana Hadarean; Kshitij Bansal; Dejan Jovanovic; Clark W. Barrett; Cesare Tinelli (CAV, 2014)

Deciding Local Theory Extensions via E-matching. - Kshitij Bansal; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Thomas Wies (CAV (2), 2015)

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. - Kshitij Bansal; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (IJCAR, 2016)

Decision Procedures for Finite Sets with Cardinality, and Local Theories Extensions. - Kshitij Bansal (2016)

Automatic Generation of Precise and Useful Commutativity Conditions. - Kshitij Bansal; Eric Koskinen; Omer Tripp (TACAS (1), 2018)

Automatic Generation of Precise and Useful Commutativity Conditions (Extended Version). - Kshitij Bansal; Eric Koskinen; Omer Tripp (CoRR, 2018)

Reasoning with Finite Sets and Cardinality Constraints in SMT. - Kshitij Bansal; Clark W. Barrett; Andrew Reynolds 001; Cesare Tinelli (Log. Methods Comput. Sci., 2018)

HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. - Kshitij Bansal; Sarah M. Loos; Markus N. Rabe; Christian Szegedy; Stewart Wilcox (ICML, 2019)

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). - Kshitij Bansal; Sarah M. Loos; Markus N. Rabe; Christian Szegedy; Stewart Wilcox (CoRR, 2019)

Learning to Reason in Large Theories without Imitation. - Kshitij Bansal; Sarah M. Loos; Markus N. Rabe; Christian Szegedy (CoRR, 2019)

Graph Representations for Higher-Order Logic and Theorem Proving. - Aditya Paliwal; Sarah M. Loos; Markus N. Rabe; Kshitij Bansal; Christian Szegedy (AAAI, 2020)

Mathematical Reasoning in Latent Space. - Dennis Lee 003; Christian Szegedy; Markus N. Rabe; Sarah M. Loos; Kshitij Bansal (ICLR, 2020)

Reducing Commutativity Verification to Reachability with Differencing Abstractions. - Eric Koskinen; Kshitij Bansal (CoRR, 2020)

Language Modeling for Formal Mathematics. - Markus N. Rabe; Dennis Lee 003; Kshitij Bansal; Christian Szegedy (CoRR, 2020)

Synthesizing Precise and Useful Commutativity Conditions. - Kshitij Bansal; Eric Koskinen; Omer Tripp (J. Autom. Reason., 2020)

Mathematical Reasoning via Self-supervised Skip-tree Training. - Markus Norman Rabe; Dennis Lee 003; Kshitij Bansal; Christian Szegedy (ICLR, 2021)

Decomposing Data Structure Commutativity Proofs with $m !n$-Differencing. - Eric Koskinen; Kshitij Bansal (VMCAI, 2021)

CodeGemma: Open Code Models Based on Gemma. - Heri Zhao; Jeffrey Hui; Joshua Howland; Nam Nguyen; Siqi Zuo; Andrea Hu; Christopher A. Choquette-Choo; Jingyue Shen; Joe Kelley; Kshitij Bansal; Luke Vilnis; Mateo Wirth; et al. (CoRR, 2024)