Evènement pour le groupe Séminaire Méthodes Formelles

Date 2019-06-18  11:00-12:00
TitreGeneric and Complete Algorithms for Straight-Line String Constraints 
RésuméPath-feasibility is an important problem in the symbolic execution of string-manipulating programs. A symbolic path is given as a finite, loop-free sequence of assertions and assignments and the task is to find concrete instantiations of the symbolic variables that satisfy all assertions along the path. If such instantiations are found, then the path is feasible. Such a path may witness an error in the program being analysed. Recent research has identified a number of string operations that can be supported by path-feasibility algorithms. We contribute two semantic conditions, which, if satisfied by the assertions and assignments in the program, imply decidability of the path-feasibility problem. This decidability is shown via a generic feasibility-checking algorithm. We have implemented this algorithm in a tool OSTRICH, which checks satisfiability of straight-line string constraints (paths). We have compared this tool with other leading solvers over a wide range of popular benchmarks. OSTRICH is competitive on well-supported benchmarks, while also increasing the expressivity and extensibility of the string-constraints supported. 
OrateurMatthew Hague 
UrlUniversity of London 

Aucun document lié à cet événement.

Retour à l'index