|
|
Close Help | ||||||||||||||
An important technique for analyzing programs (e.g., with the goal of finding test cases) is symbolic execution, that is, the execution of a given program not for one specific input, but for all inputs that lead the program through the same path. Tools for symbolic execution (e.g., the tool ''Symbolic Path Finder'' used at NASA) use constraint solvers to analyze the resulting paths. The goal of the thesis is to improve and adapt such constraint solvers for their use in symbolic code execution.
Starting point: Mateus Borges, Marcelo d'Amorim, Saswat Anand, David Bushnell, Corina Pasareanu: Symbolic Execution with Interval Constraint Solving and Meta-heuristic Search
