Contacts

Symbolic execution [4] is a popular program analysis technique which executes programs on unspecified inputs by using symbolic inputs instead of concrete data. Traditional applications of symbolic execution include test case generation and error detection. A recent development, Probabilistic symbolic execution (PSE) [2], aims to compute the probability of a target event to occur by computing the probability of the program paths leading to its occurrence. Both techniques are dependent on constraint solvers to check the satisfiability of the explored paths. PSE also further needs a model counter to compute the number of possible solutions for the analyzed constraints. The goal of this seminar is to: • Investigate the current techniques and tools for constraint solving/model counting of strings that compose the current state-of-art. A starting point for this can be found in [1, 3, 5, 6]. • Evaluate a selected subset of the tools found in the previous step with small experiments. References [1] Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Automata-based model counting for string constraints. [2] Antonio Filieri, Corina S. Păsăreanu, and Willem Visser. Reliability analysis in symbolic pathfinder. I