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): Dominik Winterer, Eelco Visser

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

Displayed time zone: Central Time (US & Canada) change

17:00 - 18:20
R-6OOPSLA at SPLASH-I +12h
Chair(s): Filip Niksic Google, Adam Welc Uber Technologies
17:00
20m
Talk
Adding Interactive Visual Syntax to Textual Code
OOPSLA
Leif Andersen Northeastern University, Michael Ballantyne Northeastern University, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
17:20
20m
Talk
Deductive Optimization of Relational Data Storage
OOPSLA
Jack Feser Massachusetts Institute of Technology, Sam Madden Massachusetts Institute of Technology, Nan Tang QCRI HBKU, Armando Solar-Lezama Massachusetts Institute of Technology
Link to publication DOI Media Attached
17:40
20m
Talk
Inter-theory Dependency Analysis for SMT String Solvers
OOPSLA
Minh-Thai Trinh Advanced Digital Sciences Center, Duc-Hiep Chu National University of Singapore, Joxan Jaffar National University of Singapore
Link to publication DOI Media Attached
18:00
20m
Talk
Macros for Domain-Specific Languages
OOPSLA
Michael Ballantyne Northeastern University, Alexis King Northwestern University, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

05:00 - 06:20
R-6OOPSLA at SPLASH-I
Chair(s): Dominik Winterer ETH Zurich, Eelco Visser Delft University of Technology
05:00
20m
Talk
Adding Interactive Visual Syntax to Textual Code
OOPSLA
Leif Andersen Northeastern University, Michael Ballantyne Northeastern University, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
05:20
20m
Talk
Deductive Optimization of Relational Data Storage
OOPSLA
Jack Feser Massachusetts Institute of Technology, Sam Madden Massachusetts Institute of Technology, Nan Tang QCRI HBKU, Armando Solar-Lezama Massachusetts Institute of Technology
Link to publication DOI Media Attached
05:40
20m
Talk
Inter-theory Dependency Analysis for SMT String Solvers
OOPSLA
Minh-Thai Trinh Advanced Digital Sciences Center, Duc-Hiep Chu National University of Singapore, Joxan Jaffar National University of Singapore
Link to publication DOI Media Attached
06:00
20m
Talk
Macros for Domain-Specific Languages
OOPSLA
Michael Ballantyne Northeastern University, Alexis King Northwestern University, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached