| Título: | Static analysis and certifcation of safety properties of memory usage |
| Autores: | Peña Marí, Ricardo |
| Tipo de documento: | texto impreso |
| Fecha de publicación: | 2010-06-16 |
| Palabras clave: | Estado = Presentado , Materia = Ciencias: Informática: Lenguajes de programación , Tipo = Ponencia o Póster de Seminario , Congreso , etc |
| Resumen: |
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 y Computació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 he worked 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-school students. 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 of international conferences, has been the project leader of several competitive projects of the Spanish National Plan, and has been a member of several European Union funded projects. His research areas are functional language design and implementation, functional-parallel programming, static analysis, program certifcation, and proof-carrying code.' |
Ejemplares
| Estado |
|---|
| ningún ejemplar |
