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