SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Wed 25 Oct 2023 17:12 - 17:30 at Room I - probabilistic Chair(s): Chandrakana Nandi

We present a new algorithm for solving string constraints. The algorithm builds upon a recent method for solving word equations and regular constraints that interprets string variables as languages rather than strings and, consequently, mitigates the combinatorial explosion that plagues other approaches. We extend the approach to handle linear integer arithmetic length constraints by combination with a known principle of equation alignment and splitting, and by extension to other common types of string constraints, yielding a fully-fledged string solver. The ability of the framework to handle unrestricted disequalities even extends one of the largest decidable classes of string constraints, the chain-free fragment. We integrate our algorithm into a DPLL-based SMT solver. The performance of our implementation is competitive and even significantly better than state-of-the-art string solvers on several established benchmarks obtained from applications in verification of string programs.

Wed 25 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
probabilisticOOPSLA at Room I
Chair(s): Chandrakana Nandi Certora
16:00
18m
Talk
A Deductive Verification Infrastructure for Probabilistic Programs
OOPSLA
Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
DOI
16:18
18m
Talk
A Gradual Probabilistic Lambda Calculus
OOPSLA
Wenjia Ye University of Hong Kong, Matías Toro University of Chile, Federico Olmedo University of Chile
DOI
16:36
18m
Talk
Lower Bounds for Possibly Divergent Probabilistic Programs
OOPSLA
Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingshuai Chen Zhejiang University, Han Su Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Naijun Zhan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Link to publication DOI Pre-print
16:54
18m
Talk
Exact Recursive Probabilistic Programming
OOPSLA
David Chiang University of Notre Dame, Colin McDonald University of Notre Dame, Chung-chieh Shan Indiana University
DOI
17:12
18m
Talk
Solving String Constraints with Lengths by StabilizationDistinguished Paper
OOPSLA
Yu-Fang Chen Academia Sinica, David Chocholatý Brno University of Technology, Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Juraj Síč Brno University of Technology
DOI