Almorzando con Marcelo Frias
Título: Hacia el Analisis Escalable de Codigo Basado en SAT-Solving
| Qué |
|
|---|---|
| Cuándo |
12/06/2007 de 12:45 pm a 02:00 pm |
| Dónde | Laboratorio 5 |
| Agregar evento al calendario |
vCal
iCal
|
- Disertante: Marcelo Frias
- Título: Hacia el Analisis Escalable de Codigo Basado en SAT-Solving
- Resumen:
El análisis de código consiste en el estudio de las propiedades que el comportamiento de un programa puede tener. Se desea chequear que ciertas propiedades indeseables no ocurren, o que propiedades deseables sí ocurren. Una técnica que se utiliza con éxito limitado en la actualidad consiste en la traducción de una porción de código y la propiedad a chequear a una fórmula proposicional y utilizar un SAT solver para analizar si la proposición así obtenida se satiface o no. En esta charla describiré las limitaciones que hoy en día tiene el SAT-solving como estrategia para el análisis de código, y describiré las líneas de investigación que se llevan adelante en el grupo de métodos formales relacionales para superar estas limitaciones.
- Bio:
Realizó su Doctorado en la Pontificia Universidad Católica de Rio de Janeiro. Actualmente es Profesor Asociado Interino del DC, e Investigador del CONICET. Ganó el Premio Houssay a la Investigación Científica y Tecnológica de la SECyT en 2003. Actualmente es miembro del Comité de Programa de las siguientes conferencias: Formal Methods 2008, ICFEM 2008, WICSA 2008, ASSE 2007, IDEAS 2008.
