EXPRESSION: A Language for Architecture Exploration through Compiler/Simulator Retargetability. - Ashok Halambi; Peter Grun; Vijay Ganesh 001; Asheesh Khare; Nikil D. Dutt; Alexandru Nicolau (DATE, 1999)

Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. - Vijay Ganesh 001; Sergey Berezin; David L. Dill (FMCAD, 2002)

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. - Sergey Berezin; Vijay Ganesh 001; David L. Dill (TACAS, 2003)

A Decision Procedure for Bit-Vectors and Arrays. - Vijay Ganesh 001; David L. Dill (CAV, 2007)

Decision procedures for bit-vectors, arrays and integers. - Vijay Ganesh 001 (2007)

EXE: Automatically Generating Inputs of Death. - Cristian Cadar; Vijay Ganesh 001; Peter M. Pawlowski; David L. Dill; Dawson R. Engler (ACM Trans. Inf. Syst. Secur., 2008)

Taint-based directed whitebox fuzzing. - Vijay Ganesh 001; Tim Leek; Martin C. Rinard (ICSE, 2009)

HAMPI: a solver for string constraints. - Adam Kiezun; Vijay Ganesh 001; Philip J. Guo; Pieter Hooimeijer; Michael D. Ernst (ISSTA, 2009)

jFuzz: A Concolic Whitebox Fuzzer for Java. - Karthick Jayaraman; David Harvison; Vijay Ganesh 001; Adam Kiezun (NASA Formal Methods, 2009)

HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection. - Vijay Ganesh 001; Adam Kiezun; Shay Artzi; Philip J. Guo; Pieter Hooimeijer; Michael D. Ernst (CAV, 2011)

Automatic error finding in access-control policies. - Karthick Jayaraman; Vijay Ganesh 001; Mahesh V. Tripunitara; Martin C. Rinard; Steve J. Chapin (CCS, 2011)

ARBAC Policy for a Large Multi-National Bank - Karthick Jayaraman; Vijay Ganesh 001; Mahesh V. Tripunitara; Martin C. Rinard; Steve J. Chapin (CoRR, 2011)

SMT-LIB Sequences and Regular Expressions. - Nikolaj S. Bjørner; Vijay Ganesh 001; Raphaël Michel; Margus Veanes (SMT@IJCAR, 2012)

An SMT-based approach to automated configuration. - Raphaël Michel; Arnaud Hubaux; Vijay Ganesh 001; Patrick Heymans (SMT@IJCAR, 2012)

Word Equations with Length Constraints: What's Decidable? - Vijay Ganesh 001; Mia Minnes; Armando Solar-Lezama; Martin C. Rinard (Haifa Verification Conference, 2012)

Automatic input rectification. - Fan Long; Vijay Ganesh 001; Michael Carbin; Stelios Sidiroglou; Martin C. Rinard (ICSE, 2012)

Lynx: A Programmatic SAT Solver for the RNA-Folding Problem. - Vijay Ganesh 001; Charles W. O'Donnell; Mate Soos; Srinivas Devadas; Martin C. Rinard; Armando Solar-Lezama (SAT, 2012)

Cryptographic Path Hardening: Hiding Vulnerabilities in Software through Cryptography - Vijay Ganesh 001; Michael Carbin; Martin C. Rinard (CoRR, 2012)

STP/HAMPI and Computer Security - Vijay Ganesh 001 (CoRR, 2012)

HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. - Adam Kiezun; Vijay Ganesh 001; Shay Artzi; Philip J. Guo; Pieter Hooimeijer; Michael D. Ernst (ACM Trans. Softw. Eng. Methodol., 2012)

Z3-str: a z3-based string solver for web application analysis. - Yunhui Zheng; Xiangyu Zhang 001; Vijay Ganesh 001 (ESEC/SIGSOFT FSE, 2013)

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints. - Vijay Ganesh 001; Mia Minnes; Armando Solar-Lezama; Martin C. Rinard (CoRR, 2013)

Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies. - Karthick Jayaraman; Mahesh V. Tripunitara; Vijay Ganesh 001; Martin C. Rinard; Steve J. Chapin (ACM Trans. Inf. Syst. Secur., 2013)

Impact of Community Structure on SAT Solver Performance. - Zack Newsham; Vijay Ganesh 001; Sebastian Fischmeister; Gilles Audemard; Laurent Simon 001 (SAT, 2014)

Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442). - Cristian Cadar; Vijay Ganesh 001; Raimondas Sasnauskas; Koushik Sen (Dagstuhl Reports, 2014)

Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints. - Yunhui Zheng; Vijay Ganesh 001; Sanu Subramanian; Omer Tripp; Julian Dolby; Xiangyu Zhang 001 (CAV (1), 2015)

Short Paper: The Meaning of Attack-Resistant Systems. - Vijay Ganesh 001; Sebastian Banescu; Martín Ochoa (PLAS@ECOOP, 2015)

Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers. - Jia Hui Liang; Vijay Ganesh 001; Ed Zulkoski; Atulan Zaman; Krzysztof Czarnecki 001 (Haifa Verification Conference, 2015)

SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers. - Zack Newsham; William Lindsay; Vijay Ganesh 001; Jia Hui Liang; Sebastian Fischmeister; Krzysztof Czarnecki 001 (SAT, 2015)

SAT-based analysis of large real-world feature models is easy. - Jia Hui (Jimmy) Liang; Vijay Ganesh 001; Krzysztof Czarnecki 001; Venkatesh Raman 001 (SPLC, 2015)

The Meaning of Attack-Resistant Programs. - Vijay Ganesh 001; Sebastian Banescu; Martín Ochoa (CoRR, 2015)

Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). - Armin Biere; Vijay Ganesh 001; Martin Grohe; Jakob Nordström; Ryan Williams 001 (Dagstuhl Reports, 2015)

Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. - Jia Hui Liang; Vijay Ganesh 001; Pascal Poupart; Krzysztof Czarnecki 001 (AAAI, 2016)

Code obfuscation against symbolic execution attacks. - Sebastian Banescu; Christian S. Collberg; Vijay Ganesh 001; Zack Newsham; Alexander Pretschner (ACSAC, 2016)

Manifold: an SMT-based declarative language for electronic and microfluidic design synthesis. - Murphy Berzish; Asif Khan; Atulan Zaman; Vijay Ganesh 001; Derek Rayside (CASCON, 2016)

Combining static analysis and targeted symbolic execution for scalable bug-finding in application binaries. - Riyad Parvez; Paul A. S. Ward; Vijay Ganesh 001 (CASCON, 2016)

MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. - Edward Zulkoski; Vijay Ganesh 001; Krzysztof Czarnecki 001 (IJCAI, 2016)

Learning Rate Based Branching Heuristic for SAT Solvers. - Jia Hui Liang; Vijay Ganesh 001; Pascal Poupart; Krzysztof Czarnecki 001 (SAT, 2016)

MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures. - Curtis Bright; Vijay Ganesh 001; Albert Heinle; Ilias S. Kotsireas; Saeed Nejati; Krzysztof Czarnecki 001 (SC²@SYNASC, 2016)

Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs. - Steven T. Stewart; Derek Rayside; Vijay Ganesh 001; Krzysztof Czarnecki 001 (VSTTE, 2016)

Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion. - Vijay Ganesh 001; Murphy Berzish (CoRR, 2016)

A Solver for a Theory of Strings and Bit-vectors. - Sanu Subramanian; Murphy Berzish; Yunhui Zheng; Omer Tripp; Vijay Ganesh 001 (CoRR, 2016)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks. - Martín Ochoa; Sebastian Banescu; Cynthia Disenfeld; Gilles Barthe; Vijay Ganesh 001 (EuroS&P, 2017)

Z3str3: A string solver with theory-aware heuristics. - Murphy Berzish; Vijay Ganesh 001; Yunhui Zheng (FMCAD, 2017)

A solver for a theory of string and bit-vectors. - Sanu Subramanian; Murphy Berzish; Vijay Ganesh 001; Omer Tripp (ICSE (Companion Volume), 2017)

Preface. - Matthew England 001; Vijay Ganesh 001 (SC²@ISSAC, 2017)

An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate. - Jia Hui Liang; Hari Govind V. K.; Pascal Poupart; Krzysztof Czarnecki 001; Vijay Ganesh 001 (SAT, 2017)

A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers. - Saeed Nejati; Zack Newsham; Joseph Scott; Jia Hui Liang; Catherine H. Gebotys; Pascal Poupart; Vijay Ganesh 001 (SAT, 2017)

Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions. - Saeed Nejati; Jia Hui Liang; Catherine H. Gebotys; Krzysztof Czarnecki 001; Vijay Ganesh 001 (VSTTE, 2017)

Z3str3: A String Solver with Theory-aware Branching. - Murphy Berzish; Yunhui Zheng; Vijay Ganesh 001 (CoRR, 2017)

Relating Complexity-theoretic Parameters with SAT Solver Performance. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Robert Robere; Jia Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CoRR, 2017)

Z3str2: an efficient solver for strings, regular expressions, and length constraints. - Yunhui Zheng; Vijay Ganesh 001; Sanu Subramanian; Omer Tripp; Murphy Berzish; Julian Dolby; Xiangyu Zhang 001 (Formal Methods Syst. Des., 2017)

Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures. - Edward Zulkoski; Curtis Bright; Albert Heinle; Ilias S. Kotsireas; Krzysztof Czarnecki 001; Vijay Ganesh 001 (J. Autom. Reason., 2017)

A SAT+CAS Method for Enumerating Williamson Matrices of Even Order. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (AAAI, 2018)

StringFuzz: A Fuzzer for String Solvers. - Dmitry Blotsky; Federico Mora 002; Murphy Berzish; Yunhui Zheng; Ifaz Kabir; Vijay Ganesh 001 (CAV (2), 2018)

The Proof Complexity of SMT Solvers. - Robert Robere; Antonina Kolokolova; Vijay Ganesh 001 (CAV (2), 2018)

Algebraic Fault Attack on SHA Hash Functions Using Programmatic SAT Solvers. - Saeed Nejati; Jan Horácek; Catherine H. Gebotys; Vijay Ganesh 001 (CP, 2018)

The Effect of Structural Measures and Merges on SAT Solver Performance. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Jia Hui Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CP, 2018)

Learning-Sensitive Backdoors with Restarts. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Robert Robere; Jia Hui Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CP, 2018)

An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate. - Jia Liang; Hari Govind V. K.; Pascal Poupart; Krzysztof Czarnecki 001; Vijay Ganesh 001 (IJCAI, 2018)

Enumeration of Complex Golay Pairs via Programmatic SAT. - Curtis Bright; Ilias S. Kotsireas; Albert Heinle; Vijay Ganesh 001 (ISSAC, 2018)

The Satisfiability of Word Equations: Decidable and Undecidable Theories. - Joel D. Day; Vijay Ganesh 001; Paul He; Florin Manea; Dirk Nowotka (RP, 2018)

Machine Learning-Based Restart Policy for CDCL SAT Solvers. - Jia Hui Liang; Chanseok Oh; Minu Mathew; Ciza Thomas; Chunxiao Li 002; Vijay Ganesh 001 (SAT, 2018)

Predicting SAT Solver Performance on Heterogeneous Hardware. - Zack Newsham; Vijay Ganesh 001; Sebastian Fischmeister (POS@SAT, 2018)

The SAT+CAS paradigm and the Williamson conjecture. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (ACM Commun. Comput. Algebra, 2018)

The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability. - Joel D. Day; Vijay Ganesh 001; Paul He; Florin Manea; Dirk Nowotka (CoRR, 2018)

Applying Computer Algebra Systems and SAT Solvers to the Williamson Conjecture. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (CoRR, 2018)

A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples. - Curtis Bright; Dragomir Z. Ðokovic; Ilias S. Kotsireas; Vijay Ganesh 001 (AAAI, 2019)

SAT solvers and computer algebra systems: a powerful combination for mathematics. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (CASCON, 2019)

CDCL(Crypto) SAT solvers for cryptanalysis. - Saeed Nejati; Vijay Ganesh 001 (CASCON, 2019)

Interpolating Strong Induction. - Hari Govind Vediramana Krishnan; Yakir Vizel; Vijay Ganesh 001; Arie Gurfinkel (CAV (2), 2019)

MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract. - William Zhang; Sebastian Banescu; Leonardo Pasos; Steven T. Stewart; Vijay Ganesh 001 (ISSRE, 2019)

Theory and practice of string solvers (invited talk abstract). - Adam Kiezun; Philip J. Guo; Pieter Hooimeijer; Michael D. Ernst; Vijay Ganesh 001 (ISSTA, 2019)

Effective Problem Solving Using SAT Solvers. - Curtis Bright; Jürgen Gerhard; Ilias S. Kotsireas; Vijay Ganesh 001 (MC, 2019)

Accelerated Learning of Predictive Runtime Monitors for Rare Failure. - Reza Babaee; Vijay Ganesh 001; Sean Sedwards (RV, 2019)

On the Proof Complexity of MCSAT. - Gereon Kremer; Erika Ábrahám; Vijay Ganesh 001 (SC-square@SIAM AG, 2019)

The SAT+CAS method for combinatorial search with applications to best matrices. - Curtis Bright; Dragomir Z. Dokovic; Ilias S. Kotsireas; Vijay Ganesh 001 (Ann. Math. Artif. Intell., 2019)

An Empirical Investigation of Randomized Defenses against Adversarial Attacks. - Yannik Potdevin; Dirk Nowotka; Vijay Ganesh 001 (CoRR, 2019)

SMTIBEA: a hybrid multi-objective optimization algorithm for configuring large constrained software product lines. - Jianmei Guo; Jia Hui Liang; Kai Shi 006; Dingyu Yang; Jingsong Zhang; Krzysztof Czarnecki 001; Vijay Ganesh 001; Huiqun Yu (Softw. Syst. Model., 2019)

On the Unreasonable Effectiveness of SAT Solvers. - Vijay Ganesh 001; Moshe Y. Vardi (Beyond the Worst-Case Analysis of Algorithms, 2020)

LGML: Logic Guided Machine Learning (Student Abstract). - Joseph Scott; Maysum Panju 001; Vijay Ganesh 001 (AAAI, 2020)

A Machine Learning Based Splitting Heuristic for Divide-and-Conquer Solvers. - Saeed Nejati; Ludovic Le Frioux; Vijay Ganesh 001 (CP, 2020)

Online Bayesian Moment Matching based SAT Solver Heuristics. - Haonan Duan 002; Saeed Nejati; George Trimponias; Pascal Poupart; Vijay Ganesh 001 (ICML, 2020)

Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem. - Curtis Bright; Kevin K. H. Cheung; Brett Stevens; Ilias S. Kotsireas; Vijay Ganesh 001 (IJCAI, 2020)

Nonexistence Certificates for Ovals in a Projective Plane of Order Ten. - Curtis Bright; Kevin K. H. Cheung; Brett Stevens; Ilias S. Kotsireas; Vijay Ganesh 001 (IWOCA, 2020)

Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers. - Chunxiao Li 002; Noah Fleming; Marc Vinyals; Toniann Pitassi; Vijay Ganesh 001 (SAT, 2020)

Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving. - Vincent Vallade; Ludovic Le Frioux; Souheib Baarir; Julien Sopena; Vijay Ganesh 001; Fabrice Kordon (SAT, 2020)

Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers. - Joseph Scott; Federico Mora 002; Vijay Ganesh 001 (SMT, 2020)

Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Vijay Ganesh 001 (SMT, 2020)

BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers. - Joseph Scott; Federico Mora 002; Vijay Ganesh 001 (VSTTE, 2020)

A nonexistence certificate for projective planes of order ten with weight 15 codewords. - Curtis Bright; Kevin K. H. Cheung; Brett Stevens; Dominique Roy; Ilias S. Kotsireas; Vijay Ganesh 001 (Appl. Algebra Eng. Commun. Comput., 2020)

LogicGAN: Logic-guided Generative Adversarial Networks. - Laura Graves; Vineel Nagisetty; Joseph Scott; Vijay Ganesh 001 (CoRR, 2020)

Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks. - Sebastian Johann Wetzel; Roger G. Melko; Joseph Scott; Maysum Panju 001; Vijay Ganesh 001 (CoRR, 2020)

LGML: Logic Guided Machine Learning. - Joseph Scott; Maysum Panju 001; Vijay Ganesh 001 (CoRR, 2020)

A Length-aware Regular Expression SMT Solver. - Murphy Berzish; Mitja Kulczynski; Federico Mora 002; Florin Manea; Joel D. Day; Dirk Nowotka; Vijay Ganesh 001 (CoRR, 2020)

Logic Guided Genetic Algorithms. - Dhananjay Ashok; Joseph Scott; Sebastian Johann Wetzel; Maysum Panju 001; Vijay Ganesh 001 (CoRR, 2020)

Applying computer algebra systems with SAT solvers to the Williamson conjecture. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (J. Symb. Comput., 2020)

New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (IEEE Trans. Inf. Theory, 2020)

Logic Guided Genetic Algorithms (Student Abstract). - Dhananjay Ashok; Joseph Scott; Sebastian Johann Wetzel; Maysum Panju 001; Vijay Ganesh 001 (AAAI, 2021)

A SAT-based Resolution of Lam's Problem. - Curtis Bright; Kevin K. H. Cheung; Brett Stevens; Ilias S. Kotsireas; Vijay Ganesh 001 (AAAI, 2021)

Amnesiac Machine Learning. - Laura Graves; Vineel Nagisetty; Vijay Ganesh 001 (AAAI, 2021)

An SMT Solver for Regular Expressions and Linear Arithmetic over String Length. - Murphy Berzish; Mitja Kulczynski; Federico Mora 002; Florin Manea; Joel D. Day; Dirk Nowotka; Vijay Ganesh 001 (CAV (2), 2021)

String Theories Involving Regular Membership Predicates: From Practice to Theory and Back. - Murphy Berzish; Joel D. Day; Vijay Ganesh 001; Mitja Kulczynski; Florin Manea; Federico Mora 002; Dirk Nowotka (WORDS, 2021)

Z3str4: A Multi-armed String Solver. - Federico Mora 002; Murphy Berzish; Mitja Kulczynski; Dirk Nowotka; Vijay Ganesh 001 (FM, 2021)

BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning. - Joseph Scott; Trishal Sudula; Hammad Rehman; Federico Mora 002; Vijay Ganesh 001 (FM, 2021)

On the Hierarchical Community Structure of Practical Boolean Formulas. - Chunxiao Li 002; Jonathan Chung 003; Soham Mukherjee; Marc Vinyals; Noah Fleming; Antonina Kolokolova; Alice Mu; Vijay Ganesh 001 (SAT, 2021)

Logic Solvers and Machine Learning: The Next Frontier (keynote abstract). - Vijay Ganesh 001 (SC-Square@SIAM AG, 2021)

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (TACAS (2), 2021)

On the Hierarchical Community Structure of Practical SAT Formulas. - Chunxiao Li 002; Jonathan Chung 003; Soham Mukherjee; Marc Vinyals; Noah Fleming; Antonina Kolokolova; Alice Mu; Vijay Ganesh 001 (CoRR, 2021)

Complex Golay pairs up to length 28: A search via computer algebra and programmatic SAT. - Curtis Bright; Ilias S. Kotsireas; Albert Heinle; Vijay Ganesh 001 (J. Symb. Comput., 2021)

A Solver + Gradient Descent Training Algorithm for Deep Neural Networks. - Dhananjay Ashok; Vineel Nagisetty; Christopher Srinivasa; Vijay Ganesh 001 (IJCAI, 2022)

Gas Gauge: A Security Analysis Tool for Smart Contract Out-of-Gas Vulnerabilities. - Behkish Nassirzadeh; Huaiying Sun; Sebastian Banescu; Vijay Ganesh 001 (MARBLE, 2022)

An SC-Square Approach to the Minimum Kochen-Specker Problem. - Zhengyu Li 002; Curtis Bright; Vijay Ganesh 001 (SC-Square@FLoC, 2022)

Diversifying a Parallel SAT Solver with Bayesian Moment Matching. - Vincent Vallade; Saeed Nejati; Julien Sopena; Souheib Baarir; Vijay Ganesh 001 (SETTA, 2022)

Goose: A Meta-Solver for Deep Neural Network Verification. - Joseph Scott; Guanting Pan; Elias B. Khalil; Vijay Ganesh 001 (SMT, 2022)

When satisfiability solving meets symbolic computation. - Curtis Bright; Ilias S. Kotsireas; Vijay Ganesh 001 (Commun. ACM, 2022)

Formal Languages via Theories over Strings. - Joel D. Day; Vijay Ganesh 001; Nathan Grewal; Florin Manea (CoRR, 2022)

Machine learning and logic: a new frontier in artificial intelligence. - Vijay Ganesh 001; Sanjit A. Seshia; Somesh Jha (Formal Methods Syst. Des., 2022)

Editorial. - Zhé Hóu; Vijay Ganesh 001; Jing Sun 002 (Innov. Syst. Softw. Eng., 2022)

Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291). - Sébastien Bardin; Somesh Jha; Vijay Ganesh 001 (Dagstuhl Reports, 2022)

Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). - Olaf Beyersdorff; Armin Biere; Vijay Ganesh 001; Jakob Nordström; Andy Oertel (Dagstuhl Reports, 2022)

MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Zenodo, 2022)

Robust Training for AC-OPF (Student Abstract). - Fuat Can Beylunioglu; Mehrdad Pirnia; P. Robert Duimering; Vijay Ganesh 001 (AAAI, 2023)

Grounding Neural Inference with Satisfiability Modulo Theories. - Zifan Wang 001; Saranya Vijayakumar; Kaiji Lu; Vijay Ganesh 001; Somesh Jha; Matt Fredrikson (NeurIPS, 2023)

Learning Shorter Redundant Clauses in SDCL Using MaxSAT. - Albert Oliveras; Chunxiao Li 002; Darryl Wu; Jonathan Chung 003; Vijay Ganesh 001 (SAT, 2023)

Pierce: A Testing Tool for Neural Network Verification Solvers. - Joseph Scott; Guanting Pan; Piyush Jha; Elias B. Khalil; Vijay Ganesh 001 (VSTTE, 2023)

Learning Modulo Theories. - Matt Fredrikson; Kaiji Lu; Saranya Vijayakumar; Somesh Jha; Vijay Ganesh 001; Zifan Wang 001 (CoRR, 2023)

CGDTest: A Constrained Gradient Descent Algorithm for Testing Neural Networks. - Vineel Nagisetty; Laura Graves; Guanting Pan; Piyush Jha; Vijay Ganesh 001 (CoRR, 2023)

BertRLFuzzer: A BERT and Reinforcement Learning based Fuzzer. - Piyush Jha; Joseph Scott; Jaya Sriram Ganeshna; Mudit Singh; Vijay Ganesh 001 (CoRR, 2023)

Attention, Compilation, and Solver-based Symbolic Analysis are All You Need. - Prithwish Jana; Piyush Jha; Haoyang Ju; Gautham Kishore; Aryan Mahajan; Vijay Ganesh 001 (CoRR, 2023)

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem. - Zhengyu Li 002; Curtis Bright; Vijay Ganesh 001 (CoRR, 2023)

Formal Languages via Theories over Strings: An Overview of Some Recent Results. - Joel D. Day; Vijay Ganesh 001; Florin Manea (Bull. EATCS, 2023)

Limits of CDCL Learning via Merge Resolution. - Noah Fleming; Vijay Ganesh 001; Antonina Kolokolova; Chunxiao Li 002; Marc Vinyals (Electron. Colloquium Comput. Complex., 2023)

Towards more efficient methods for solving regular-expression heavy string constraints. - Murphy Berzish; Joel D. Day; Vijay Ganesh 001; Mitja Kulczynski; Florin Manea; Federico Mora 002; Dirk Nowotka (Theor. Comput. Sci., 2023)

On the Expressive Power of String Constraints. - Joel D. Day; Vijay Ganesh 001; Nathan Grewal; Florin Manea (Proc. ACM Program. Lang., 2023)

Algorithm selection for SMT. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Int. J. Softw. Tools Technol. Transf., 2023)

Publisher Correction: Algorithm selection for SMT. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Int. J. Softw. Tools Technol. Transf., 2023)

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract). - Zhengyu Li 002; Curtis Bright; Vijay Ganesh 001 (AAAI, 2024)

A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract). - Conor Duggan; Zhengyu Li 002; Curtis Bright; Vijay Ganesh 001 (AAAI, 2024)

BertRLFuzzer: A BERT and Reinforcement Learning Based Fuzzer (Student Abstract). - Piyush Jha; Joseph Scott; Jaya Sriram Ganeshna; Mudit Singh; Vijay Ganesh 001 (AAAI, 2024)

CountChain: A Decentralized Oracle Network for Counting Systems. - Behkish Nassirzadeh; Albert Heinle; Stefanos Leonardos; M. Anwar Hasan; Vijay Ganesh 001 (Blockchain, 2024)

CoTran: An LLM-Based Code Translator Using Reinforcement Learning with Feedback from Compiler and Symbolic Execution. - Prithwish Jana; Piyush Jha; Haoyang Ju; Gautham Kishore; Aryan Mahajan; Vijay Ganesh 001 (ECAI, 2024)

A SAT Solver + Computer Algebra Attack on the Minimum Kochen-Specker Problem. - Zhengyu Li 002; Curtis Bright; Vijay Ganesh 001 (IJCAI, 2024)

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis. - Zhengyang Lu 002; Stefan Siemer; Piyush Jha; Joel D. Day; Florin Manea; Vijay Ganesh 001 (IJCAI, 2024)

AdChain: Decentralized Header Bidding. - Behkish Nassirzadeh; Albert Heinle; Stefanos Leonardos; M. Anwar Hasan; Vijay Ganesh 001 (MARBLE, 2024)

AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems. - Piyush Jha; Zhengyu Li 002; Zhengyang Lu 002; Curtis Bright; Vijay Ganesh 001 (CoRR, 2024)

A Reinforcement Learning based Reset Policy for CDCL SAT Solvers. - Chunxiao Li 002; Charlie Liu; Jonathan Chung 003; Zhengyang Lu 002; Piyush Jha; Vijay Ganesh 001 (CoRR, 2024)

RLSF: Reinforcement Learning via Symbolic Feedback. - Piyush Jha; Prithwish Jana; Arnav Arora; Vijay Ganesh 001 (CoRR, 2024)

Extended Resolution Clause Learning via Dual Implication Points. - Sam Buss; Jonathan Chung 003; Vijay Ganesh 001; Albert Oliveras (CoRR, 2024)

Can Transformers Reason Logically? A Study in SAT Solving. - Leyan Pan; Vijay Ganesh 001; Jacob D. Abernethy; Chris Esposo; Wenke Lee (CoRR, 2024)

LLMStinger: Jailbreaking LLMs using RL fine-tuned LLMs. - Piyush Jha; Arnav Arora; Vijay Ganesh 001 (CoRR, 2024)

A Closer Look at the Expressive Power of Logics Based on Word Equations. - Joel D. Day; Vijay Ganesh 001; Nathan Grewal; Matthew Konefal; Florin Manea (Theory Comput. Syst., 2024)

Btor2-SelectMC (HWMCC 2024 Submission). - Zhengyang John Lu; Po-Chun Chien; Nian-Ze Lee; Vijay Ganesh 001 (Zenodo, 2024)

Btor2-SelectMC (HWMCC 2024 Submission). - Zhengyang John Lu; Po-Chun Chien; Nian-Ze Lee; Vijay Ganesh 001 (Zenodo, 2024)

Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract). - Zhengyang Lu 002; Po-Chun Chien; Nian-Ze Lee; Vijay Ganesh 001 (AAAI, 2025)

LLM Stinger: Jailbreaking LLMs Using RL Fine-Tuned LLMs (Student Abstract). - Piyush Jha; Arnav Arora; Vijay Ganesh 001 (AAAI, 2025)

Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. - Zhengyang Lu 002; Po-Chun Chien; Nian-Ze Lee; Arie Gurfinkel; Vijay Ganesh 001 (CAV (1), 2025)

Robustness of Deep Learning Classification to Adversarial Input on GPUs: Asynchronous Parallel Accumulation Is a Source of Vulnerability. - Sanjif Shanmugavelu; Mathieu Taillefumier; Christopher Culver; Vijay Ganesh 001; Oscar R. Hernandez; Ada Sedova (Euro-Par (2), 2025)

Improving and Understanding the Power of Satisfaction-Driven Clause Learning. - Albert Oliveras; Chunxiao (Ian) Li; Darryl Wu; Jonathan Chung 003; Vijay Ganesh 001 (J. Artif. Intell. Res., 2025)

Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems. - Zhengyu Li 002; Conor Duggan; Curtis Bright; Vijay Ganesh 001 (CoRR, 2025)

Abstractions-of-Thought: Intermediate Representations for LLM Reasoning in Hardware Design. - Matthew DeLorenzo; Kevin Tieu; Prithwish Jana; Piyush Jha; Dileep Kalathil; Vijay Ganesh 001; Jeyavijayan Rajendran (CoRR, 2025)

Towards AI-assisted Neutrino Flavor Theory Design. - Jason Benjamin Baretz; Max Fieg; Vijay Ganesh 001; Aishik Ghosh; V. Knapp-Perez; Jake Rudolph; Daniel Whiteson (CoRR, 2025)

Novel tree-search method for synthesizing SMT strategies. - Zhengyang John Lu; Joel D. Day; Piyush Jha; Paul Sarnighausen-Cahn; Stefan Siemer; Florin Manea; Vijay Ganesh 001 (Acta Informatica, 2025)