Cuatro publicaciones realizadas por investigadores del Instituto IMDEA Software han sido aceptadas para su publicación en la 27 edición del congreso internacional sobre verificación asistida por ordenador, un congreso de máximo nivel en este área, celebrado este año en San Francisco, CA. Estas cuatro publicaciones estan entre las 68 seleccionadas de un total de 250 presentadas.
César Sánchez, investigador del Instituto IMDEA Software, tiene una publicación sobre verificación de hiperpropiedades por comprobación de modelos, junto con Bernd Finkbeiner y Markus Rabe de Instituto IMDEA Software. Esta publicación caracteriza de forma precisa la complejidad del problema de comprobación de modelos par hiperpropiedades, y muestra como utilizar las herramientas de comprobación de modelos existentes para manejar especificaciones de hiperpropiedades, con aplicaciones en seguridad, simetría, y teoría de la programación.
Boris Köpf, investigador del Instituto IMDEA Software, tiene una publicación conjunta con Klaus von Gleissenthall ((Instituto IMDEA Software) y Andrey Rybalchenko (Instituto IMDEA Software) sobre verificación de propiedades cuantitativas de programas, tales como límites en utilización de recursos y fugas de información. La principal novedad tecnológica es un algoritmo basado en SMT para la síntesis de interpolantes con restricciones cardinales que se basan en la teoría de conteo de puntos enteros en politopos simbólicos.
Una contribución de Michael Emmi, investigador del Instituto IMDEA Software, describe el desarrollo de una herramienta para la identificación de errores de concurrencia en aplicaciones Android, un trabajo conjunto con Burcu Kulahcioglu Ozkan y Serdar Tasiran de la Koç University en Turquía.
Pierre Ganty, investigador del Instituto IMDEA Software, tiene un artículo sobre verificación automática en sistemas asíncronos de memoria compartida, en colaboración con A. Durand-Gasselin, J. Esparza de Instituto IMDEA Software y R. Majumdar de Instituto IMDEA Software. Su trabajo clasifica los problemas de verificación de propiedades de “liveness” en los sistemas asíncronos de memoria compartida desde un punto de vista computacional. Estos sistemas se caracterizan por presentar un proceso líder y un número arbitrario de otros contribuyentes anónimos e idénticos. Los procesos se comunicac entre sí a través de un registro compartido con valor acotado.
Más información en el sitio web del congreso.
