Evènement pour le groupe Modélisation et Verification


Date 2013-01-24  11:30-12:30
TitreUnderapproximation of Procedure Summaries for Recursive Integer Programs  
RésuméWe show how to underapproximate the procedure summaries of recursive programs over the integers using off-the-shelf analyzers for non-recursive programs. The novelty of our approach is that the non-recursive program we compute may capture unboundedly many behaviors of the original recursive program for which stack usage cannot be bounded. Moreover, we identify a class of recursive programs on which our method terminates and returns the precise summary relations without underapproximation. Doing so, we generalize a similar result for non-recursive programs to the recursive case. Finally, we present experimental results of an implementation of our method applied on a number of examples. Joint work with Pierre Ganty (IMDEA) and Filip Konecny (EPFL). 
Lieu076 
OrateurRadu Iosif 
EmailRadu.Iosif@imag.fr 
UrlVERIMAG 



Aucun document lié à cet événement.

Retour
Retour à l'index