Strings represent one of the most common and most intricate data-types found in software programs, with correct string processing often being a decisive factor for correctness and security properties. This has led to a wide range of recent research results on how to analyse programs operating on strings, using methods like testing, fuzzing, symbolic execution, abstract interpretation, or model checking, and, increasingly, support for strings is also added to constraint solvers and SMT solvers. In this paper, we focus on the verification of software programs with strings using model checking. We give a survey of the existing approaches to handle strings in this context, and propose methods based on algebraic data-types, Craig interpolation, and automata learning.

Philipp Rümmer is an Associate Professor at the IT Department of Uppsala University, Sweden. He received his PhD from Gothenburg University in 2008, and is generally interested in any kind of technology that is useful for program verification. Over the years, he has contributed to deductive verification methods (including the tools KeY and Boogie), developed software model checkers (including Eldarica and JayHorn), worked on theorem provers and SMT solvers (leading to a zoo of solvers, among others inhabited by Princess, Norn, Sloth, Ostrich, Trau, UppSAT), and investigated the application of verification methods in domains like Embedded Systems and Security. In 2013 he received the Oscar Award, Uppsala University’s most prestigious award for young researchers, and in 2014 the Best-paper Award of IJCAR.