Algorithmic Verification of String-Manipulating Programs (AV-SMP)

This is the page for our project AV-SMP. It was supported by ERC Starting Grant (2017 - 2022) and by Amazon Research Award (2021). The project is still very much active.

The purpose of the project is to study foundational issues concerning string constraint solving, and their applications to verification of string-manipulating programs. This project was hosted from November 2018 to February 2020 at University of Oxford, and from March 2021 to October 2022 at TU Kaiserslautern.

Check out our string solver OSTRICH supporting complex string constraints (including transducers). OSTRICH was ranked #1 in SMT Competition 2022 for the category (unsat, string theory, largest contribution); see here. OSTRICH won QF_S in SMT-COMP 2023!

Members

Current Members

• Prof. Anthony W. Lin (Principal Investigator)
• Mr. Pascal Bergstraßer (PhD Student)
• Mr. Oliver Markgraf (PhD Student)

Past Members

• Dr. Daniel Stan (Postdoc Researcher, now tenured assistant professor at Epita, France)
• Mr. Chih-Duo Hong (Postdoc Researcher)
• Dr. Shuanglong Kan (Postdoc Researcher, now researcher at Certik)
• Dr. Xuan-Bach Le (Postdoc Researcher, now Postdoc at Nanyang Technical Uni, Singapore)
• Dr. Muhammad Najib (Postdoc Researcher, now Lecturer at Heriot-Watt Uni, UK)
• Dr. Reino Niskanen (Postdoc Researcher, now Lecturer at Liverpool John Moores University, UK)

Collaborators

• Prof. Pablo Barcelo (Institute for Mathematical and Computational Engineering, PUC Chile & IMFD Chile)
• Dr. Taolue Chen (Birkbeck, University of London, UK)
• Prof. Matthew Hague (Royal Holloway, University of London, UK)
• Dr. Lukas Holik (Brno University of Technology, Czechia)
• Prof. Rupak Majumdar (MPI-SWS, Germany)
• Dr. Philipp Rümmer (Uppsala University, Sweden)
• Prof. Tomas Vojnar (Brno University of Technology, Czechia)
• Dr. Zhilin Wu (Chinese University of Science, China)

Tools

• OSTRICH.
• SLOTH
• CertiStr

Press

• AV-SMP was featured in Inspired Research Newsletter Summer 2018 - Issue 12. Here for the excerpt. Here for the original publication.

Publications

• Reasoning on Data Words over Numeric Domains. In Logic in Computer Science (LICS), 2022. (Diego Figueira and Anthony W. Lin).
• Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification. In Logic in Computer Science (LICS), 2022. (Pascal Bergstraesser, Moses Ganardi, Anthony W. Lin and Georg Zetzsche).
• Data Path Queries over Embedded Graph Databases. In Principles of Database Systems (PODS), 2022. (Diego Figueira, Artur Jeż, and Anthony W. Lin)
• CertiStr: A Certified String Solver. In CPP 2022.
  (Joint with Shuanglong Kan, Philipp Ruemmer, and Micha Schrader) [Distinguished Paper Award]
• Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. In POPL 2022. (Joint with T. Chen, M. Hague, Z. Han, D. Hu, S. Kan, A. Lamas, A. Lin, P. Ruemmer, and Z. Wu)
• Regular Model Checking Revisited. In Bengt Jonsson’s Festschrift, 2022. (Anthony Lin and Philipp Ruemmer).
• Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility. Accepted in LMCS in 2021. (Anthony W. Lin and Rupak Majumdar). Extended abstract was published in ATVA’18.
• Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems. In AAMAS’21. (Daniel Stan and Anthony W. Lin)
• Parameterized Synthesis with Safety Properties. In APLAS’20. (Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, and Daniel Neider)
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. In ATVA’20. (Taolue Chen, Matt Hague, Denghang Hu, Anthony Lin, Philipp Ruemmer, and Zhilin Wu)
• Monadic Decomposition in Integer Linear Arithmetic. In IJCAR’20. (Matthew Hague, Anthony Lin, Philipp Ruemmer, and Zhilin Wu)
• Learning-Based Synthesis of Safety Controllers. In FMCAD’19. (Daniel Neider and Oliver Markgraf)
• Probabilistic Bisimulation for Parameterized Systems - with applications to verifying anonymous protocols. In CAV’19. (Chih-Duo Hong, Anthony W. Lin Rupak Majumdar, and Philipp Ruemmer)
• Monadic Decomposability of Regular Relations. . In ICALP’19. (with Pablo Barcelo, Chih-Duo Hong, Xuan Bach Le, Anthony W. Lin, and Reino Niskanen)
• CSS Minification via Constraint Solving. In ACM Transactions of Programming Languages and Systems 2019 (presented at POPL’19). (Matthew Hague, Anthony W. Lin, and Chih-Duo Hong)
• Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. In POPL’19. (Taolue Chen, Matt Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu)
• Complexity Analysis of Tree Share Structure. In APLAS’18. (Xuan-Bach Le, Aquinas Hobor, and Anthony W. Lin)
• What is Decidable About String Constraints with ReplaceAll Function, In POPL’18. (Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin and Zhilin Wu)
• String Constraints with Concatenation and Transducers Solved Efficiently, In POPL’18. (Lukas Holik, Petr Janku, Anthony W. Lin, Philipp Ruemmer, and Tomas Vojnar)