BiCi

Abstract: In the past several years, Satisfiability Modulo Theories (SMT) solvers have been extended for reasoning about quantifier-free constraints in the theory of unbounded strings and regular expressions. Although decidability of this theory is unknown, many of these solvers are highly efficient for constraints that commonly occur in practice. This talk overviews the main algorithms used by the SMT solver CVC4 for handling string constraints. We focus on its core theory solver for strings, regular expressions and length constraints. We then cover its more advanced features, including its finite model finding strategy for strings of bounded length, context-dependent simplification for extended string functions and its support for regular expression elimination.

Abstract: I plan to discuss the role of constraint solving and model counting for string constraints in the context of symbolic execution, with an application to side channel analysis.

Abstract: A word equation is given by two strings over disjoint alphabets of letters and variables and we ask whether there is a substitution that makes the sides of the equation truly equal as strings. Recently, a new PSPACE solution to this problem was proposed, it is based on the recompression technique, which compresses simple substrings of the equation (compression of pairs ab by a new symbol c, where a ≠ b, and compression of maximal substrings a^l by a new symbol a_l) and modifying the equation so that such operations are sound; those modifications boil down to substitutions X → aX and X → Xb. The analysis focuses on the way the equation is stored and changed rather than on the combinatorics of words. This approach greatly simplified many existing proofs and algorithms. Moreover, it is also applicable to restricted cases (for instance: one-variable equations, but also compressed string testing) and to generalisations (regular constraints, involution, partial commutation, tree equations, etc.).

Abstract: Path-feasibility is an important problem in the symbolic execution of string-manipulating programs. A symbolic path is given as a finite, loop-free sequence of assertions and assignments and the task is to find concrete instantiations of the symbolic variables that satisfy all assertions along the path. If such instantiations are found, then the path is feasible. Such a path may witness an error in the program being analysed. Recent research has identified a number of string operations that can be supported by path-feasibility algorithms. We contribute two semantic conditions, which, if satisfied by the assertions and assignments in the program, imply decidability of the path-feasibility problem. This decidability is shown via a generic feasibility-checking algorithm. We have implemented this algorithm in a tool OSTRICH, which checks satisfiability of straight-line string constraints (paths). We have compared this tool with other leading solvers over a wide range of popular benchmarks. OSTRICH is competitive on well-supported benchmarks, while also increasing the expressivity and extensibility of the string-constraints supported.

Abstract: In this talk I will give an overview on a way of defining classes of word relations called Synchronized relations. This framework yields an infinite number of classes living within the well-studied class of Rational relations, among which we can find the classes Automatic, Recognizable, or length-preserving relations. A natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, which can be seen as regular languages L over the alphabet {1,2} x A, where (i,a) is interpreted as reading letter a from tape i. Thus, a word w of the language L denotes the pair (u_1,u_2) in A* x A* in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations due to Nivat’s Theorem (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1,2}. In this way, for each regular language C contained in {1,2}*, one obtains a class Rel(C) of relations. I will show some recent results on this collection of classes of relations, based on joint work with María Emilia Descotte, Santiago Figueira, Leonid Libkin, and Gabriele Puppis.

Abstract: Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this talk, we discuss how regular functions, either on finite or infinite words can be described using regular transducer expressions (RTE). The basic building blocks of these expressions are simple and natural functions. I will touch upon two such building blocks : one which uses the composition operation, and one which does not.

Abstract: Consider the following one-player game. Take a well-formed sequence of opening and closing brackets (a word in the Dyck language). As a move, the player can pair any opening bracket with any closing bracket to its right, erasing them. The goal is to re-pair (erase) the entire sequence, and the cost of a strategy is measured by its width: the maximum number of nonempty segments of symbols (separated by blank space) seen during the play. In the talk, I will discuss this re-pairing game and upper and lower bounds on the minimum width sufficient for re-pairing. I will also talk about connections between this game on strings and automata theory.

Abstract: Writing a scripts can be a tedious and error-prone task, especially for end users. When requesting help, users will often continually provide more examples until their intentions are understood. Recognizing this, we developed an interactive programming by example framework, called StriSynth, that allows end-users to automatically generate stand-alone scripts by incrementally providing examples, and receive feedback throughout the process. To investigate the impact of StriSynth and programming by example paradigm on real-world users, we built a study around StriSynth, and recruited 27 working IT professionals to participate. In our study we asked the users to complete three tasks with StriSynth, and the same three tasks with PowerShell, a traditional scripting language. We found that, although our participants completed the tasks more quickly with StriSynth, they reported that they believed PowerShell to be a more helpful tool.

Abstract: Identifying decidable fragments in the theory of strings has been a quest for researchers in both theoretical and practical avenues. The latter has become more of significant interest with the recent attempts in automating reasoning community to give the best effort towards the automation of reasoning over undecidable theories. A major difficulty in reasoning over strings is that, in general, the satisfiability problem of any reasonably comprehensive theory of character strings is undecidable. However, one can indicate several restricted, but still quite useful, fragments of the theory of strings that are decidable. Recent research on the string theory has focused on identifying decidable fragments suitable for automated analysis and developing efficient solvers for them. This talk presents our attempts towards the search for decidable fragments in the theory of string with the string calculus defined in CVC4. We will explore the approaches we tried to this extent and share where these efforts led us.

Abstract: OSTRICH is an expressive, easy, efficient, and extensible string solver recently developed for path feasibility problem of string-manipulating programs with complex string operations. The crux of OSTRICH is a simple decision procedure which propagates the regular language constraints in a backward manner via the regularity-preserving pre-image computation. Nevertheless, although OSTRICH is expressive in the sense of string operations involving only the string data type, it still does not support the operations involving both the string and integer data type, e.g. string length, substring, and indexof functions. In this talk, I will report our ongoing work to extend OSTRICH to integer data type. This extension is built on integer cost register automata (ICRA), a nondeterministic variant of cost register automata introduced by Alur et. al. (LICS 2013), where the cost domain is interpreted as the set of integers. Then the decision procedure of OSTRICH can be seamlessly extended by replacing finite-state automata with ICRA. With this extension, OSTRICH is then capable of solving string constraints involving both the string and integer data types, i.e. string constraints that contain string length, indexof, and substring functions, in addition to those operations already supported by the current version of OSTRICH.

Abstract: This talk gives an overview on techniques for solving computationally hard problems for nondeterministic automata: language inclusion/equivalence checking and automata minimization. We focus on nondeterministic Buchi automata and NFAs, but the techniques carry over to tree-automata. Some techniques use logical subsumption to narrow the search space for a counterexample: antichain methods and congruence base methods. Other techniques use generalized types of simulation preorders (multi-pebble and lookahead simulations) to manipulate automata, e.g., merging state, removing states/transitions or witnessing language inclusion outright. Finally, we'll discuss some open questions and challenges. A collection of current papers and tools is available at www.languageinclusion.org. See also https://lmcs.episciences.org/5189

Abstract: Strings with length constraints are prominent in software security analysis. In this talk, we will present logic circuit representation for (nondeterministic) finite automata to support various string and automata manipulation operations. It enables both counterexample generation and filter synthesis in string constraint solving. By using the new data structure, automata with large state spaces and/or alphabet sizes can be efficiently represented. The representation is further augmented with length encoding. By converting string and length constraints into a dependency graph of manipulations over length-encoded automata, a symbolic model checker for infinite state systems can be leveraged as an engine for the analysis of string and length constraints. Experiments show that the method has its unique capability of handling complex string and length constraints not solvable by other methods.

Abstract: We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability problem for nondeterministic finite automata, and then carefully encoding this as a propositional logic satisfiability problem, which we then solve using the well-known Glucose SAT-solver. This approach has the advantage of allowing for the natural inclusion of additional linear length constraints.