%0 Generic
%A Peña Marí, Ricardo
%T Static analysis and certifcation of safety properties of memory usage
%D 2010
%U https://hdl.handle.net/20.500.14352/45912
%X he talk summarizes the work done by the author and his group in the last few years on the functional language Safe. This is an experimental language aimed at platforms with limited memory resources, and at a proof-carrying code framework.  Its programming model allows explicit deallocation of data structures, and its runtime system additionally supports regions, i.e. disjoint parts of the heap allocated and deallocated in constant time, which replace the more traditional garbage collector. The Safe compiler is equipped with a battery of static analyses and with a special type system which are able to frst ensure, and then to formally certify, safety runtime properties such as absence of dangling pointers, and bounded memory consumption. Compiled programs are endowed with Isabelle/HOl scripts proving that these properties actually hold. Ricardo Peña Marí is a full Professor in Computer Science at the "Sistemas Informáticos yComputación" Department of the "Universidad Complutense de Madrid". Up to 1991, he was Associate Professor at the "Universidad Politécnica de Cataluña", and prior to that heworked for two companies in the telecommunication and clothing industries as project leader of several sofware developments. He is the author of "Diseño de Programas",Pearson-Prentice Hall 2005, a textbook for undergraduate Computer Engineers, of "De Euclides a Java: historia de los algoritmos y de los lenguajes de programación", Nivola,2006, a broad-audience book on the history of programming languages and algorithms, and co-author of "La Informática a todo mega", Ediciones SM 2000, a book for high-schoolstudents. He is co-author of more than 50 peer reviewed papers published in international journals and conferences, belongs or has belonged to several Program Committees ofinternational conferences, has been the project leader of several competitive projects of the Spanish National Plan, and has been a member of several European Union fundedprojects. His research areas are functional language design and implementation, functional-parallel programming, static analysis, program certifcation, and proof-carrying code.'
%~