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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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)
• (bib entry) (abstract) (code and slides)
• 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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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
• (bib entry) (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. [paper] [slides]
• SMT 2016 (presentation-only paper). Coimbra, Portugal. July 2016
• Yunhui Zheng, A String, Regular Expression, and Integer Solver for Bug-finding and Security.
• HCSS 2016. Annapolis, USA. May 2016
• Yunhui Zheng, Effective Search-space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints.
• 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