Důležitá metoda pro analýzu programů (např. s cílem nalezení testovacích případů) je symbolická exekuce, tj. exekuce program nejen pro jeden specifický vstup, ale pro množinu všech vstupů, které provádí program určitým pořadím řádků. Přístroje pro symbolickou analýzu (např. ''Symbolic Path Finder'' americké kosmonautické organizace NASA) používají určité řešiče pro analýzu jejich výsledků. Cílem této práce je zlepšení a upravení takových řešičů pro jejich využití v symbolické exekuci kódu.
Výchozí bod: Mateus Borges, Marcelo d'Amorim, Saswat Anand, David Bushnell, Corina Pasareanu: Symbolic Execution with Interval Constraint Solving and Meta-heuristic Search