SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 17:40 - 18:00 at SPLASH-I - R-6 Chair(s): Filip Niksic, Adam Welc
Fri 20 Nov 2020 05:40 - 06:00 at SPLASH-I - R-6 Chair(s): Eelco Visser, Dominik Winterer

Solvers in the framework of Satisfiability Modulo Theories (SMT) have been widely successful in practice. Recently there has been an increasing interest in solvers for string constraints to address security issues in web programming, for example. To be practically useful, the solvers need to support an expressive constraint language over unbounded strings, and in particular, over string lengths. Satisfiability checking for these formulas, especially in the SMT context, is very hard; it is generally undecidable for a rich fragment. In this paper, we propose a form of dependency analysis for a rich fragment of string constraints including high-level operations such as length, contains to deal with their inter-theory interaction so as to solve them more efficiently. We implement our dependency analysis in the string theory of the Z3 solver to obtain a new one, called S3N. Finally, we demonstrate the superior performance of S3N over state-of-the-art string solvers such as Z3str3, CVC4, S3P, and Z3 on several large industrial-strength benchmarks.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: R-6OOPSLA at SPLASH-I +12h
Chair(s): Filip NiksicGoogle, Adam WelcUber Technologies
17:00 - 17:20
Talk
OOPSLA
Leif AndersenNortheastern University, Michael BallantyneNortheastern University, Matthias FelleisenNortheastern University
Link to publication DOI Media Attached
17:20 - 17:40
Talk
OOPSLA
John FeserMassachusetts Institute of Technology, Sam MaddenMassachusetts Institute of Technology, Nan TangQCRI HBKU, Armando Solar-LezamaMassachusetts Institute of Technology
Link to publication DOI Media Attached
17:40 - 18:00
Talk
OOPSLA
Minh-Thai TrinhAdvanced Digital Sciences Center, Duc-Hiep ChuNational University of Singapore, Joxan JaffarNational University of Singapore
Link to publication DOI Media Attached
18:00 - 18:20
Talk
OOPSLA
Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University
Link to publication DOI Media Attached

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: R-6OOPSLA at SPLASH-I
Chair(s): Eelco VisserDelft University of Technology, Dominik WintererETH Zurich
05:00 - 05:20
Talk
OOPSLA
Leif AndersenNortheastern University, Michael BallantyneNortheastern University, Matthias FelleisenNortheastern University
Link to publication DOI Media Attached
05:20 - 05:40
Talk
OOPSLA
John FeserMassachusetts Institute of Technology, Sam MaddenMassachusetts Institute of Technology, Nan TangQCRI HBKU, Armando Solar-LezamaMassachusetts Institute of Technology
Link to publication DOI Media Attached
05:40 - 06:00
Talk
OOPSLA
Minh-Thai TrinhAdvanced Digital Sciences Center, Duc-Hiep ChuNational University of Singapore, Joxan JaffarNational University of Singapore
Link to publication DOI Media Attached
06:00 - 06:20
Talk
OOPSLA
Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University
Link to publication DOI Media Attached