Publications / Presentations

Publications

• Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis
  Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel D. Day, Florin Manea, and Vijay Ganesh
  In the Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI 2024), Jeju, South Korea, August 3-9, 2024
  (bibentry) (abstract)
  


• A Closer Look at the Expressive Power of Logics Based on Word Equations
  Joel D. Day, Vijay Ganesh, Nathan Grewal, Matthew Konefal, and Florin Manea
  Theoretical Computer Science, Volume 68, pp 322-379, June 2024
  (bibentry) (abstract)
  


• On the Expressive Power of String Constraints
  Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea
  Proceedings of the ACM on Programming Languages (POPL), Volume 7, Issue POPL, Article No 10, pp 278-308, January 2023
  (abstract)
  


• Towards more efficient methods for solving regular-expression heavy string constraints
  Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Nathan Grewal, Florin Manea, Federico Mora, and Dirk Nowotka
  Theoretical Computer Science, Volume 943, pp 50-72, January 2023
  (bibentry) (abstract)
  


• Z3str4: A Multi-armed String Solver
  Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, and Vijay Ganesh
  24th International Symposium on Formal Methods (FM 2021), Virtual Event, November 20–26, 2021
  (bibentry) (abstract)
  


• String Theories involving Regular Membership Predicates: From Practice to Theory and Back
  Murphy Berzish, Joel Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka
  13th International Conference on WORDS (WORDS 2021), Rouen, France, September 13-17, 2021
  (bibentry) (abstract)
  


• Z3str4: A Solver for Theories over Strings
  Murphy Berzish
  PhD. Thesis (2021)
  (bibentry) (abstract)
  


• An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
  Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, and Vijay Ganesh
  33rd International Conference on Computer-Aided Verification (CAV 2021), Los Angeles, California, USA, July 18-23, 2021
  (bibentry) (abstract)
  


• Theory and Practice of String Solvers
  Adam Kiezun, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst, and Vijay Ganesh
  Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019), Beijing, China, on July 15-19, 2019
  (bibentry) (abstract)
  


• The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability
  Joel Day, Vijay Ganesh, Paul He, Florin Manea, and Dirk Nowotka
  The 12th International Conference on Reachability Problems (RP 2018), Marseille, France, September 24-26, 2018
  (bibentry) (abstract)
  


• StringFuzz: A Fuzzer for String Solvers
  Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh
  The 30th International Conference on Computer Aided Verification (CAV 2018), Oxford, United Kingdom, July 14-17, 2018
  (bibentry) (abstract)
  


• Z3str3: A String Solver with Theory-Aware Heuristics
  Murphy Berzish, Vijay Ganesh, and Yunhui Zheng
  Formal Methods in Computer-Aided Design (FMCAD), Vienna, Austria, October 2017
  (bibentry) (abstract)
  


• Z3str2: An Efficient Solver for Strings, Regular Expressions, and Length Constraints
  Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Murphy Berzish, Julian Dolby and Xiangyu Zhang
  Formal Methods in Systems Design, Volume 50, Issue 2, pp.249-288, June 2017
  Invited paper at the Formal Methods in Systems Design Journal (FMSD 2017)
  (bibentry) (abstract)
  


• A Solver for a Theory of Strings and Bit-Vectors
  Murphy Berzish, Sanu Subramanian, Omer Tripp, and Vijay Ganesh
  Accepted for publication at International Conference on Software Engineering (ICSE 2017) Poster Track, Buenos Aires, Argentina, May 20-28, 2017
  


• Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion
  Vijay Ganesh and Murphy Berzish
  arXiv preprint 1605.094442, May 2016
  (bibentry) (abstract)
  


• 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
  The 27th International Conference on Computer Aided Verification (CAV 2015), Artifact Evaluated, July 2015
  Paper selected for Formal Methods for System Design Journal, Special Issue dedicated to the Best Papers at CAV’15
  (bibentry) (abstract)
  


• Z3-str: a z3-based string solver for web application analysis
  Yunhui Zheng, Xiangyu Zhang and Vijay Ganesh
  In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2013) , Saint Petersburg, Russia, Aug. 18-26, 2013
  (bibentry) (abstract)
  


• 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, Volume 21, Issue 4 (TOSEM 2012)
  Invited Paper to the ACM TOSEM Journal 2012
  (bibentry) (abstract)
  


• 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
  (bibentry) (abstract)
  


• 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
  (bibentry) (abstract)
  


• 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
  ACM Distinguished Paper Award 2009
  (bibentry) (abstract)
  

Presentations

• Vijay Ganesh, Theory and Practice of String Solvers [slides]
  ISSTA 2019 Keynote Talk. Beijing, China. July 2019
  


• Murphy Berzish, Length-Aware Regular Expression Solving in Z3str3 [slides]
  MOSCA 2019 Bertinoro, Italy. May 2019
  


• Murphy Berzish, Architectural Overview of Z3 and Z3str3 [slides]
  


• Vijay Ganesh, Z3str3: A String Solver with Theory-Aware Heuristics [slides]
  SMT 2017 (presentation-only paper). Heidelberg, Germany. July 2017
  


• Murphy Berzish, Z3str3: A DPLL(T) Solver for a Theory of Strings and Integers [slides]
  HCSS 2017 Annapolis, USA. May 2016
  


• Murphy Berzish, Z3strBV: A Solver for a Theory of Strings and Bit-vectors [slides]
  SMT 2016 (presentation-only paper). Coimbra, Portugal. July 2016
  


• Yunhui Zheng, A String, Regular Expression, and Integer Solver for Bug-finding and Security [slides]
  HCSS 2016 Annapolis, USA. May 2016
  


• Yunhui Zheng, Effective Search-space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints [slides]
  CAV 2015 San Francisco, USA. Jul 2015
  


• Yunhui Zheng, Z3-str: a Z3-based string solver for web application analysis
  ESEC/FSE 2013 Saint Petersburg, Russia. Aug 2013