Master Thesis MSTR-2016-63

BibliographyNoller, Yannic: Model counting of string constraints for probabilistic symbolic execution.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Master Thesis No. 63 (2016).
69 pages, english.
Abstract

Probabilistic symbolic execution is a static analysis technique aiming at quantifying the probability of a target event occurring during a program execution; it exploits symbolic execution to identify the conditions on the program inputs leading to the occurrence of the target event and then model counting to quantify their probability. While efficient methods exist for model counting of numeric constraints, only limited results have been obtained for counting string constraints. The constraints are indeed first encoded in a corresponding accepting automaton; then the number of accepting paths of the automaton is quantified via a convenient generating function. The encoding in the form of automata limits the expressiveness of the formalism used for constraint specification to constructs mappable into automata, for an exact model count. Furthermore, the encoding of disjunctions requires the parallel composition of the automata representing the disjuncts, leading to an exponential growth in the size of the resulting automata. This thesis introduces the usage of SMT solvers to count the models of a string constraint by leveraging a standard smtlib interface. Several algorithms for both exact and approximate model counting of string constraints are defined and compared. The different solutions are implemented on top of the SMT solver CVC4 and evaluated on a set of established benchmarks, demonstrating the increased expressiveness with respect to previous approaches and improved performance on several classes of problems.

Full text and
other links
Volltext
Department(s)University of Stuttgart, Institute of Software Technology, Software Reliability and Security
Superviser(s)Filieri, Dr. Antonio
Entry dateJune 5, 2019
   Publ. Computer Science