Papers in reverse chronological order (also available on Google Scholar and DBLP)

2022

• Robust Training of ML Boosted AC-OPF
  Fuat Can Beylunioglu, Mehrdad Pirnia, P. Robert Duimering, and Vijay Ganesh
  In submission

2021

• Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
  Curtis Bright, Ilias Kotsireas, Albert Heinle, and Vijay Ganesh
  Journal of Symbolic Computation (JSC 2021), 102: 153-172, 2021
  (bib entry) (abstract)
  
  
• BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning
  Joseph Scott, Trishal Sudula, Hammad Rehman, Federico Mora, and Vijay Ganesh
  In the Proceedings of the 24th International Symposium on Formal Methods (FM 2021), Virtual Conference, Nov 20-26, 2021
  (bib entry) (abstract)
  
  
• Z3str4: A Multi-armed String Solver
  Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, and Vijay Ganesh
  In the Proceedings of the 24th International Symposium on Formal Methods (FM 2021), Virtual Conference, Nov 20-26, 2021
  (bib entry) (abstract)
  
  
• String Theories involving Regular Membership Predicates: From Theory to Practice and Back
  Murphy Berzish, Joel Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka
  In the Proceedings of the 13th International Conference on the Combinatorics of Words (WORDS 2021), Virtual Conference, Sep 13-17, 2021
  (bib entry) (abstract)
  
  
• An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
  Murphy Berzish, Mitja Kulczynski, Federico Mora, Joel Day, Florin Manea, Dirk Nowotka, and Vijay Ganesh
  In the Proceedings of the 33rd International Conference on Computer Aided Verification (CAV 2021), Virtual Conference, July 20-23, 2021
  (bib entry) (abstract)
  
  
• On the Hierarchical Community Structure of Practical Boolean Formulas
  Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh
  In the Proceedings of the 24th International Conference on Theory and Application of Satisfiability Testing (SAT 2021), Virtual Conference, July 5-9, 2021
  (bib entry) (abstract)
  
  
• MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
  Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh
  27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Virtual Conference, March 27 - Apr 1, 2021
  (bib entry) (abstract)
  
  
• Logic Guided Genetic Algorithms
  Dhananjay Ashok, Joseph Scott, Sebastian Wetzel, Maysum Panju, and Vijay Ganesh
  In the Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), Virtual Conference, Feb 2-9, 2021
  (bib entry) (abstract)
  
  
• Amnesiac Machine Learning
  Laura Graves, Vineel Nagisetty, and Vijay Ganesh
  In the Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), Virtual Conference, Feb 2-9, 2021
  (bib entry) (abstract)
  
  
• A SAT-based Resolution of Lam's Problem
  Curtis Bright, Kevin Cheung, Brett Stevens, Ilias Kotsireas, and Vijay Ganesh
  In the Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), Virtual Conference, Feb 2-9, 2021
  (bib entry) (abstract)

2020

• On The Unreasonable Effectiveness of SAT Solvers (Book Chapter)
  Vijay Ganesh and Moshe Vardi
  In Beyond the Worst-case Analysis of Algorithms, Tim Roughgarden (Ed.), Cambridge University Press, 2020
  (bib entry) (abstract)
  
  
• Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks
  Sebastian Wetzel, Roger Melko, Joseph Scott, Maysum Panju, and Vijay Ganesh
  Physical Review Research (PRR 2020), Volume 2, Issue 3, Sep 2020
  (bib entry) (abstract)
  
  
• A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
  Curtis Bright, Kevin K. J. Cheung, Brett Stevens, Dominique Roy, Ilias S. Kotsireas, and Vijay Ganesh
  Springer Journal of Applicable Algebra for Engineering, Communications, and Computing, 31(3-4), 195-213, 2020
  (bib entry) (abstract)
  
  
• Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
  Curtis Bright, Ilias Kotsireas, and Vijay Ganesh
  Journal of Symbolic Computation (JSC 2020), 100: 187-209, 2020
  (bib entry) (abstract)
  
  
• New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences
  Curtis Bright, Ilias S. Kotsireas, and Vijay Ganesh
  IEEE Transactions of Information Theory (ToIT 2020) 66(12): 7739-7751, 2020
  (bib entry) (abstract)
  
  
• Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
  Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, Vijay Ganesh
  In the Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI 2020), Virtual Conference, Jan 7-15, 2021
  (bib entry) (abstract)
  
  
• A Machine Learning based Splitting Heuristic for Divide-and-Conquer Solvers
  Saeed Nejati, Ludovic Le Frioux, and Vijay Ganesh
  In the Proceedings of the 26th Principles and Practice of Constraint Programming (CP 2020), Virtual Conference, Sep 7-11, 2020
  (bib entry) (abstract)
  
  
• BanditFuzz: A Reinforcement Learning based Performance Fuzzer for SMT Solvers
  Joseph Scott, Federico Mora, and Vijay Ganesh
  In the Proceedings of the 12th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2020), Virtual Conference, Jul 20-21, 2020
  (bib entry) (abstract)
  
  
• Online Bayesian Moment Matching based SAT Solver Heuristics
  Saeed Nejati, Haonan Duan, George Trimponias, Pascal Poupart, and Vijay Ganesh
  In the Proceedings of the 31st International Conference on Machine Learning (ICML 2020), Virtual Conference, Jul 12-18, 2020
  (bib entry) (abstract)
  
  
• Towards a Complexity-theoretic Understanding of Restarts in SAT Solvers
  Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh
  In the Proceedings of the 23rd International Conference on Theory and Practice of Satisfiability Testing, Virtual Conference, Jun 3-10, 2020
  (bib entry) (abstract)
  
  
• Community and LBD-based Clause Learning Sharing Policy for Parallel SAT Solving
    Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, and Fabrice Kordon
  In the Proceedings of the 23rd International Conference on Theory and Practice of Satisfiability Testing, Virtual Conference, Jun 3-10, 2020
  (bib entry) (abstract)
  
  
• Non-existence Certificates for Ovals in a Projective Plane of Order Ten
  Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, Vijay Ganesh
  In the Proceedings of 31st International Workshop on Combinatorial Algorithms (IWOCA 2020), Virtual Workshop, Jun 8-10,2020
  (bib entry) (abstract)
  
  
• Logic Guided Machine Learning (LGML)
  Joseph Scott, Maysum Panju, and Vijay Ganesh
  In the Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), New York City, New York, USA Feb 7-12, 2020
  (bib entry) (abstract)
  

2019

• SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
  Curtis Bright, Ilias Kotsireas, and Vijay Ganesh.
  In the proceedings of the 29th Annual International Conference on Computer Science and Software Engineering (CASCON 2019), Toronto, Canada, Nov 4, 2019.
  (bib entry) (abstract)
  
  
• CDCL(Crypto) SAT Solvers for Cryptanalysis
  Saeed Nejati and Vijay Ganesh.
  In the proceedings of the 29th Annual International Conference on Computer Science and Software Engineering (CASCON 2019), Toronto, Canada, Nov 4, 2019.
  (bib entry) (abstract)
  
  
• MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contracts
  William Zhang, Sebastian Banescu, Steven Stewart, Leonardo Passos, and Vijay Ganesh.
  In the Proceedings of the 30th International Symposium on Software Reliability Engineering (ISSRE 2019), Berlin, Germany, Oct 28 – 31, 2019.
  (bib entry) (abstract)
  
  
• Accelerated Learning of Predictive Runtime Monitors for Rare Failure
  Reza Babaee, Vijay Ganesh, and Sead Edwards.
  In the Proceedings of the 19th International Conference on Runtime Verification (RV 2019), Porto, Portugal, October 8-11, 2019.
  (bib entry) (abstract)
  
  
• Effective Problem Solving using SAT Solvers
  Curtis Bright, Jeurgen Gerhard, Ilias Kotsireas, and Vijay Ganesh.
  In the Proceedings of the Maple Conference (Maple 2019), Waterloo, Ontario, Canada.
  (bib entry) (abstract)
  
  
• Interpolating Strong Induction
  Hari Govind, Yakir Vizel, Vijay Ganesh, and Arie Gurfinkel.
  In the Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), New York City, New York, USA, July 15-18, 2019.
  (bib entry) (abstract)
  
  
• Theory and Practice of String Solvers (Keynote Talk)
  Adam Kiezun, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst, and Vijay Ganesh. 
  In the Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019), Beijing, China, July 15-19, 2019.
  ACM IMPACT Paper Award at ISSTA 2019
  (bib entry) (abstract)
  
  
• A SAT+CAS Approach to Finding Good Matrices: Examples and Counterexamples
  Curtis Bright, Dragomir Djokovic, Ilias Kotsireas, and Vijay Ganesh
  In the Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019), Honolulu, Hawaii, USA, January 27 – February 1, 2019.
  (bib entry) (abstract)
  
  
• New Infinite Families of Perfect Quaternion and Williamson Sequences
  Curtis Bright, Ilias Kotsireas, and Vijay Ganesh.
  Submitted to IEEE Transactions on Information Theory, (IEEE Trans on Info Theory), 2019.
  (bib entry) (abstract)
  
  
• The SAT+CAS method for Combinatorial Search with Applications to Best Matrices
  Curtis Bright, Dragomir Djokovic, Ilias Kotsireas, and Vijay Ganesh.
  Annals of Mathematics and Artificial Intelligence (AMAI 2019). Accepted. 2019.
  (bib entry) (abstract)
  
  
• Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
  Curtis Bright, Ilias Kotsireas, Albert Heinle, and Vijay Ganesh.
  Journal of Symbolic Computation (JSC 2019). Accepted. 2019.
  (bib entry) (abstract)
  
  
• SMTIBEA: A Hybrid Multi-Objective Optimization Algorithm for Configuring Large Constrained Software Product Lines
  Jianmei Guo, Jia Hui Liang, Kai Shi, Dingyu Yang, Jingsong Zhang, Vijay Ganesh, Krzysztof Czarnecki, and Huiqun Yu.
  International Journal of Software and System Modeling (SoSyM 2019), Volume 18, Issue 2, August 2019. Pages 1447-1466
  (bib entry) (abstract)
  
  
• Proof Complexity of MCSAT Solvers
  Gereon Kramer, Erika Abraham, and Vijay Ganesh.
  In the Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2019), Bern, Switzerland, 10th July 2019.
  (bib entry) (abstract)
  

2018

• The SAT+CAS Paradigm and the Williamson Conjecture (extended abstract)
  Curtis Bright, Ilias Kotsireas, and Vijay Ganesh.
  ACM Communications in Computer Algebra (ACM CCA 2018), Volume 52, Issue 3, Pages 82-84, September 2018.
  (bib entry) (abstract)
  
  
• The Satisfiability of Word Equations: Decidable and Undecidable Theories
  Joel Day, Paul He, Florin Manea, Dirk Nowotka, and Vijay Ganesh.
  In the Proceedings of the 12th International conference on Reachability Problems (RP 2018), Marseille, France, Sep 24-26, 2018.
  (bib entry) (abstract)
  
  
• Algebriac Fault Attacks on SHA Hash Functions using Programmatic SAT Solvers
  Saeed Nejati, Jan Horacek, Catherine Gebotys, and Vijay Ganesh.
  In the Proceedings of the 24th International Conference on the Principles and Practices of Constraint Programming (CP 2018), Lille, France, Aug 26-31, 2018.
  (bib entry) (abstract)
  
  
• The Effect of Structural Measures and Merges on SAT Solver Performance
  Edward Zulkoski, Ruben Martins, Christoph Wintersteiger, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh.
  In the Proceedings of the 24th International Conference on the Principles and Practices of Constraint Programming (CP 2018), Lille, France, Aug 26-31, 2018.
  (bib entry) (abstract)
  
  
• Learning Sensitive Backdoors with Restarts
  Edward Zulkoski, Ruben Martins, Christoph Wintersteiger, Robert Robere, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh.
  In the Proceedings of the 24th International Conference on the Principles and Practices of Constraint Programming (CP 2018), Lille, France, Aug 26-31, 2018.
  (bib entry) (abstract)
  
  
• Enumeration of Complex Golay Pairs via Programmatic SAT
  Curtis Bright, Albert Heinle, Ilias Kotsireas, and Vijay Ganesh.
  In the Proceedings of 43rd International Symposium of Symbolic and Algebraic Computation (ISSAC 2018), New York, New York, USA, July 16-19, 2018.
  (bib entry) (abstract)
  
  
• An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate
  Jia Hui Liang, Hari Govind, Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh.
  In the Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI 2018), Stockholm, Sweden, July 13-19, 2018.
  IJCAI 'Sister Conference Best Paper Track' Invited Paper 2018
  (bib entry) (abstract)
  
  
• The Proof Complexity of SMT Solvers
  Robert Robere, Antonina Kolkolova, and Vijay Ganesh.
  In the Proceedings of 30th International Conference on Computer Aided Verification (CAV 2018), Oxford, United Kingdom, July 14-17, 2018.
  (bib entry) (abstract)
  
  
• StringFuzz: A Fuzzer for String Solvers
  Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh.
  In the Proceedings of 30th International Conference on Computer Aided Verification (CAV 2018), Oxford, United Kingdom, July 14-17, 2018.
  (bib entry) (abstract)
  
  
• A Machine Learning based Restart Policy for CDCL SAT Solvers
  Jia Hui Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li, and Vijay Ganesh.
  In the Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018), Oxford, United Kingdom, July 9-12, 2018.
  (bib entry) (abstract)
  
  
• A SAT+CAS Method for Enumerating Williamson Matrices of Even Orders
  Curtis Bright, Ilias Kotsireas, and Vijay Ganesh.
  In the Proceedings of the 32nd  AAAI Conference on Artificial Intelligence (AAAI 2018), New Orleans, Louisiana, USA, February 2-7, 2018.
  (bib entry) (abstract)
  

2017

• Z3str3: A String Solver with Theory-aware Heuristics
  Murphy Berzish, Yunhui Zheng, and Vijay Ganesh.
  In the Proceedings of the 17th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2017), Oct 2-7, 2017, Vienna, Austria
  (bib entry) (abstract) (code and slides)
  
  
• An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate
  Jia Hui Liang, Hari Govind, Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh.
  In the Proceedings of the 20th International Conference on Theory and Application of Satisfiability Testing (SAT 2017), Aug 28 – Sep 1, 2017, Melbourne, Australia
  (bib entry) (abstract) (code and slides)
  
  
• A Propagation Rate based Splitting Heuristic for Divide-and-Conquer Solvers
  Saeed Nejati, Zack Newsham, Joe Scott, Jia Hui Liang, Catherine Gebotys, Pascal Poupart, and Vijay Ganesh.
  In the Proceedings of the 20th International Conference on Theory and Application of Satisfiability Testing (SAT 2017), Aug 28 – Sep 1, 2017, Melbourne, Australia
  (bib entry) (abstract) (code and slides)
  
  
• Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions
  Saeed Nejati, Jia Hui Liang, Catherine Gebotys, Krzysztof Czarnecki, and Vijay Ganesh.
  In the Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), July 22-23, 2017, Heidelberg, Germany
  (bib entry) (abstract) (code and slides)
  
  
• Reasoning about Probabilistic Defense Mechanisms against Remote Attacks
  Martin Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, and Vijay Ganesh
  In the Proceedings of the Second IEEE European Symposium on Security and Privacy (IEEE EuroS&P 2017), April 26-28, 2017, Paris, France
  (bib entry) (abstract) (website)
  
  
• A Solver for a Theory of Strings and Bit-vectors
  Murphy Berzish, Sanu Subramanian, Omer Tripp, and Vijay Ganesh
  In the Proceedings of the International Conference on Software Engineering (ICSE 2017), Companion Volume, May 20-28, 2017, Buenos Aires, Argentina
  (bib entry) (abstract)
  
  
• Z3str2: An Efficient Solver for Strings, Regular Expressions, and Length Constraints
  Yunhui Zheng, Murphy Berzish, Sanu E Subramanian, Omer Tripp, and Vijay Ganesh
  Invited paper at the Formal methods in Systems Design Journal (FMSD 2017), Volume 50, Number 2-3, Pages 249-288, June 2017
  (bib entry) (abstract) (code and slides)
  
  
• Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
  Edward Zulkoski, Curtis Bright, Albert Heinle, Ilias Kotsireas, Krzysztof Czarnecki, and Vijay Ganesh
  Invited paper at the Journal of Automated Reasoning (JAR 2017), Volume 58, Number 3, Pages 313-339, March 2017
  (bib entry) (abstract) (code and slides)

2016

• Code Obfuscation Against Symbolic Execution Attacks
  Sebastian Banescu, Zack Newsham, Vijay Ganesh, Christian Collberg, and Alexander Pretchner
  The 32nd Annual Computer Security Applications Conference (ACSAC 2016), Los Angeles, CA, USA, Dec 5-9, 2016
  Outstanding (Best) Paper Award @ ACSAC 2016
  (bib entry) (abstract)
  
  
• Manifold: An SMT-Based Declarative Language for Electronic and Microfluidic Design Synthesis
  Murphy Berzish, Asif Khan, Atulan Zaman, Vijay Ganesh, and Derek Rayside
  The 26th International Conference on Computer Science and Software Engineering Conference (CASCON 2016), Toronto, Canada, Oct 31-Nov 2, 2016
  (bib entry) (abstract)
  
  
• Combining Static Analysis and Targeted Symbolic Execution for Scalable Bug-finding in Application Binaries
  Riyad Parvez, Vijay Ganesh, Glenn Wurster, Joe Kirwin, and Paul Ward
  The 26th International Conference on Computer Science and Software Engineering Conference (CASCON 2016), Toronto, Canada, Oct 31-Nov 2, 2016
  (bib entry) (abstract)
  
  
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
  Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati, and Krzysztof Czarnecki
  The 18th International Conference on Computer Algebra in Scientific Computing (CASC 2016), Bucharest, Romania, Sep 19-23, 2016
  (Presented at SMT 2016 and SYNASC 2016)
  Symbolic Computation + Constraint Solving Track Invited Paper 2016
  (bib entry) (abstract) (code and slides)
  
  
• MathCheck: A Math Assistant based on a Combination of Computer Algebra Systems and SAT Solvers
  Ed Zulkoski, Vijay Ganesh, Krzysztof Czarnecki
  The 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), New York, USA, July 9-15, 2016
  IJCAI 'Sister Conference Best Paper Track' Invited Paper 2016
  (bib entry) (abstract) (code and slides)
  
  
• Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs
  Steven Stewart, Derek Rayside, Vijay Ganesh, and Krzysztof Czarnecki
  8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Toronto, Canada, July 17-18, 2016
  (bib entry) (abstract)
  
  
• Learning Rate Based Branching Heuristic for SAT Solvers
  Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki
  The 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), Bourdeaux, France, July 5-8, 2016
  (bib entry) (abstract) (code and slides)
  
  
• Exponential Recency Weighted Average Branching Heuristic for SAT Solvers
  Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki
  The 13th AAAI Conference on Artificial Intelligence (AAAI 2016), Tuscon, Arizona, USA, February 12, 2016
  (bib entry) (abstract) (code and slides)
  

2015

• Understanding the VSIDS Branching Heuristic in Conflict-driven Clause-learning SAT Solvers
  Jimmy Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, Krzysztof Czarnecki
  10th International Haifa Verification Conference (HVC 2015), Haifa, Israel, Nov 17-19, 2015
  (bib entry) (abstract)
  
  
• Predicting SAT Solver Performance on Hetergenous Hardware
  Zack Newsham, Vijay Ganesh, and Sebastian Fischmeister
  6th International Workshop on the Pragmatics of SAT, co-located with SAT 2015, Austin, Texas, USA, September 24-27, 2015
  (bib entry) (abstract)
  
  
• SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers
  Zack Newsham, William Lindsay, Vijay Ganesh, Jimmy Liang,  Sebastian Fischmeister, and Krzysztof Czarnecki
  International Conference on Satisfiability Testing (SAT 2015), Austin, Texas, USA, September 24-27, 2015
  (bib entry) (abstract) (website)
  
  
• SAT-based Analysis of Large Real-world Feature Models is Easy
  Jimmy Liang, Vijay Ganesh,  Venkatesh Raman, and Krzysztof Czarnecki
  Software Product Lines Conference (SPLC 2015), Nashville, Tennessee, USA, July 20-24, 2015
  (bib entry) (abstract)
  Best Paper Award at SPLC 2015
  
  
• Effective Search-space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints
  Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Julian Dolby and Xiangyu Zhang
  International Conference on Computer Aided Verification (CAV 2015), San Francisco, California, USA, July 18-24, 2015
  (bib entry) (abstract) (tool website)
  Invited Paper in Formal Methods for System Design (FMSD) Journal Special Issue dedicated to the Best Papers at CAV'15
  
  
• MathCheck: A Math Assistant based on a Combination of Computer Algebra Systems and SAT Solvers
  Ed Zulkoski, Vijay Ganesh, and Krzysztof Czarnecki
  International Conference on Automated Deduction (CADE 2015), Berlin, Germany, August 1-7, 2015
  (bib entry) (abstract) (tool website)
  Invited Paper in Journal of Automated Reasoning (JAR) Special Issue dedicated to the Best Papers at CADE'15
  
  
• The Meaning of Attack-resistant Programs
  Vijay Ganesh, Sebastian Banescu, Martín Ochoa
  International Workshop on Progamming Languages and Security (PLAS at ECOOP 2015), Prague, Czech Republic, July 6, 2015
  Presentation-only at International Workshop on Foundations of Computer Security (FCS at CSF 2015), Verona, Italy, July 13, 2015
  (bib entry) (abstract)
  

2014

• The Impact of Community Structure on SAT Solver Performance
  Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon
  In the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, July 14-17, 2014
  Best Student Paper Award at SAT 2014
  (bib entry) (abstract)
  

2013

• Z3-str: A Z3-based String Solver for Web Application Analysis
  Yunhui Zheng, Xiangyu Zhang and Vijay Ganesh.
  In the 9th International Foundations of Software Engineering Conference (FSE 2013), St. Petersburg, Russia, August 18-26, 2013
  Acceptance Rate: 20%
  (bib entry) (abstract) (tool website)
  
  
• (Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
  Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin Rinard.
  Invited talk at ADDCT 2013 co-held with CADE 2013
  (bib entry) (abstract)
  
  
• Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies
  Karthick Jayaraman, Mahesh Tripunitara, Vijay Ganesh, Martin C. Rinard and Steve Chapin
  ACM Transactions on Information and System Security (TISSEC 2013)
  (bib entry) (abstract) (tool website)
  

2012

• Hampi: A Solver for Word Equations over Strings, Regular Expressions and Context-free Grammar
  Vijay Ganesh, Adam Kiezun, Philip Guo, Pieter Hooimiejer and Michael Ernst
  ACM Transactions of Software Engineering Methodology (TOSEM 2012)
  (bib entry) (abstract) (tool website)
  Invited Paper to the ACM TOSEM Journal 2012
  
  
• Word Equations with Length Constraints: What's Decidable?
  Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin Rinard.
  In the 8th International Haifa Verification Conference (HVC 2012), Haifa, Israel, Nov 6-8, 2012
  (bib entry) (abstract)
  
  
• An SMT-LIB Format for Sequences and Regular Expressions
  Nikolaj Bjorner, Vijay Ganesh, Raphael Michel, and Margus Veanes
  In the 10th International Workshop for Satisfiability Modulo Theories (SMT 2012), Manchester, UK, June 22-25, 2012
  (bib entry) (abstract)
  
  
• Lynx: A Programmatic SAT Solver for the RNA-folding Problem
  Vijay Ganesh, Charles W. O'Donnell, Mate Soos, Srini Devadas, Martin Rinard, and Armando Solar-Lezama.
  In the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Trento, Italy, June 17-20, 2012
  Acceptance rate: 25%
  (bib entry) (abstract)
  
  
• Automatic Input Rectification
  Fan Long, Vijay Ganesh, Michael Carbin and Martin Rinard
  In Proceedings of the 34th International Conference on Software Engineering (ICSE 2012), Zurich, Switzerland, June 2-9 2012
  Acceptance rate: 21%
  (bib entry) (abstract)
  
  
• Cryptographic Path Hardening: Hiding Vulnerabilities in Software using Cryptography
  Vijay Ganesh, Michael Carbin and Martin Rinard
  Off-the-beaten track (OBT co-located with POPL 2012), Philadelphia, USA, January 2012
  Acceptance rate: Short paper
  (bib entry) (abstract)

2011

• Automatic Error Finding in Access-Control Policies
  Karthick Jayaraman, Vijay Ganesh, Mahesh Tripunitara, Martin C. Rinard, Steve Chapin
  In the Proceedings of the ACM Conference on Computer and Communications Security (CCS 2011) , Chicago, USA, October 2011
  Acceptance rate: 14%
  (bib entry) (abstract) (MOHAWK website)
  
  
• HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection
  Vijay Ganesh, Adam Kiezun, Shay Artzi, Philip Guo, Pieter Hooimiejer and Michael Ernst
  In Proceedings of the International Conference in Computer Aided Verification (CAV 2011), Snowbird, Utah, July 2011
  Acceptance rate: Invited Paper
  (bib entry) (abstract) (HAMPI website)
  Invited Tutorial Paper at Computer-Aided Verification Conference (CAV 2011)
  

2010 and Before

• Hampi: A Solver for String Constraints
  Adam Kiezun, Vijay Ganesh, Philip Guo, Pieter Hooimiejer and Michael Ernst
  In Proceedings of the International Symposium on Testing and Analysis (ISSTA 2009), Chicago USA, July 19-23, 2009
  Acceptance rate: 29%
  (bib entry) (abstract)
  ACM Distinguished Paper Award 2009
  
  
• Taint-based Directed Whitebox Fuzzing
  Vijay Ganesh, Tim Leek and Martin Rinard
  In Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), Vancouver, Canada, May 16-24 2009
  Acceptance rate: 12%
  (bib entry) (abstract)
  
  
• jFuzz: A Concolic WhiteBox Fuzzer for Java
  Karthick Jayaraman, David Harvison, Vijay Ganesh and Adam Kiezun
  In Proceedings of NASA Formal Methods Workshop (NFM 2009), Mountain View, CA, USA, April 2009
  
  
• EXPRESSION: A Language for Architecture Exploration through Compiler/Simulator Retargetability
  Ashok Halambi, Peter Grun, Vijay Ganesh, Asheesh Khare, Nikil Dutt and Alex Nicolau
  In Proceedings of Design, Automation and Test in Europe (DATE 2008 and 1999). Republished as "Best paper in 10 years since 1999" at DATE 2008.
  (bib entry) (abstract)
  
  
• EXE: Automatically Generating Inputs of Death
  Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Dawson Engler, and David Dill
  ACM Transactions on Information and System Security (TISSEC 2008), Volume 12, Issue 2, Article 10, December 2008
  (bib entry) (abstract)
  
  
• A Decision Procedure for Bit-vectors and Arrays
  Vijay Ganesh and David L. Dill
  In Proceedings of the International Conference in Computer Aided Verification (CAV 2007), Berlin, Germany, July 2007
  Acceptance rate: 24%
  (bib entry) (abstract) (STP website) (PhD Thesis)
  
  
• EXE: Automatically Generating Inputs of Death
  Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Dawson Engler, and David Dill
  In Proceedings of the ACM Conference on Computer and Communications Security (CCS 2006), Alexandria, Virginia, October, 2006
  Acceptance rate: 15%
  (bib entry) (abstract)
  ACM Test of Time Award @ CCS 2016
  
  
• An Online Proof-producing Decision Procedure for Mixed-Integer Linear Arithmetic
  Sergey Berezin, Vijay Ganesh, and David L. Dill
  In Proceedings of Tools and Algorithms in Construction and Analysis of Systems (TACAS 2003), Warsaw, Poland, April 2003
  Acceptance rate: 27%
  (bib entry) (abstract)
  
  
• Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods
  Sergey Berezin, Vijay Ganesh and David L. Dill
  In Proceedings of Formal Methods for Computer-Aided Design (FMCAD 2002), Portland, Oregon, November 2002
  Acceptance rate: typically < 20%
  (bib entry) (abstract)
  
  
• Overview of SAL
  Saddek Bensalem, Vijay Ganesh et al.
  In Proceedings of Langley Formal Methods Workshop (LFM 2000), Virginia, USA, 2000
  
  
• EXPRESSION: A Language for Architecture Exploration through Compiler/Simulator Retargetability
  Ashok Halambi, Peter Grun, Vijay Ganesh, Asheesh Khare, Nikil Dutt and Alex Nicolau
  In Proceedings of Design, Automation and Test in Europe (DATE 1999), Munich, Germany, March 1999
  Acceptance rate: typically < 25%
  (bib entry) (abstract)

PhD Thesis, Stanford University

• Decision Procedures for Bit-Vectors, Arrays and Integers
  Vijay Ganesh
  PhD Thesis, Computer Science Department, School of Engineering, Stanford University, Stanford, CA, USA, Sept 2007
  

Edited Volumes

• The Theory and Practice of SAT Solving
  Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams
  Dagstuhl Seminar 15171, Volume 5, Issue 4, Dagstuhl Reports, 2015
  
  
• Symbolic Execution and Constraint Solving
  Cristian Cadar, Vijay Ganesh, Raimondas Sasnauskas, and Koushik Sen
  Dagstuhl Seminar 14442, Volume 4, Issue 10, Dagstuhl Reports, 2015
  
  
• Constraints in Software Testing, Verification, and Analysis
  Vijay Ganesh and Nicky Williams
  Constraint Solving in Testing, Verification, and Analysis (CSTVA), ACM 2014

Some Old Tech-Reports

• A Decision Procedure for Fixed-width Bit-vectors
  Vijay Ganesh, Sergey Berezin, and David L. Dill
  Stanford Computer Science Department Technical Report, CSTR 2007-06, 2005
  
  
• Combination Results for Many-Sorted Theories with Overlapping Signatures
  Vijay Ganesh, Sergey Berezin, Cesare Tinelli, and David L. Dill
  Stanford Computer Science Department Technical Report, CSTR 2007-04, 2004
  
  
• Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
  Sergey Berezin, Vijay Ganesh, and David L. Dill
  Stanford Computer Science Department Technical Report, CSTR 2007-07, 2003
  
  
• Slicing SAL
  Vijay Ganesh, Hassan Saidi, and Natarajan Shankar
  Stanford Computer Science Department Technical Report, CSTR 2007-08, 1999