Browsing by Author "Pasareanu, Corina S."

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    A survey of new trends in symbolic execution for software testing and analysis
    (Springer Verlag, 2009-10) Pasareanu, Corina S.; Visser, Willem
    Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in sym- bolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multith- reading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision proce- dures for the application domain. We follow with a dis- cussion of techniques that can be used to limit the (possi- bly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping pro- grams. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.
  • Thumbnail Image
    Item
    Symbolic pathfinder for SV-COMP (Competition Contribution)
    (Springer, 2019) Noller, Yannic; Pasareanu, Corina S.; Fromherz, Aymeric; Le, Xuan-Bach D.; Visser, Willem
    This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furthermore, we comment on the competition results and we outline some directions for future work.