On Solving String Constraints
Speaker:
Mohamed Faouzi Atig, Uppsala University
Date and Time
February 28 2020, 14:15 - 15:00
Location
Polacksbacken, ITC 1211.
Abstract
String data types are present in all conventional programming and scripting languages. In fact, it is almost impossible to reason about the correctness and security of such programs without having a decision procedure for string constraints. A typical string constraint consists of word equations over string variables denoting strings of arbitrary lengths, together with constraints on (i) the length of strings, and (ii) the regular languages to which strings belong. Decidability of this general logic is still open. In this talk, we will discuss recent results on the decidability and decision procedures for string constraints. We will focus on decision procedures that are sound and complete for a well-defined fragment of string constraints. We will also cover a technique that uses a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between these modules allows increasing the precision in an automatic manner.