Publications / Presentations

Publications

• 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