Catálogo de publicaciones

Compartir en
redes sociales

Límite

Ordenar

Mostrando 10 de 166.819 registro(s)

libros

Agregar a Mi catálogo

Computing the Electrical Activity in the Heart

Autores/as: Joakim Sundnes ; Glenn Terje Lines ; Xing Cai ; Bjørn Fredrik Nielsen ; Kent-Andre Mardal ; Aslak Tveito

ISBNs: 978-3-540-33432-3 (impreso) 978-3-540-33437-8 (en línea)

Disponibilidad

Institución detectada	Año de publicación	Navegá	Descargá	Solicitá
No detectada	2006	SpringerLink

Cobertura temática: Matemáticas - Medicina clínica

actas de congreso

Agregar a Mi catálogo

Computing, Communications and Applications Conference (ComComAp)

ISBNs: 978-1-4577-1717-8 (impreso)

Disponibilidad

Institución detectada	Año de publicación	Navegá	Descargá	Solicitá
No detectada	2012	IEEE Xplore

Cobertura temática: Ingeniería eléctrica, electrónica e informática - Ingeniería de los materiales

actas de congreso

Agregar a Mi catálogo

Computing, Communications and Applications Conference (ComComAp)

ISBNs: 978-1-4673-6043-2 (impreso)

Disponibilidad

Institución detectada	Año de publicación	Navegá	Descargá	Solicitá
No detectada	2013	IEEE Xplore

Cobertura temática: Ingeniería eléctrica, electrónica e informática - Ingeniería de los materiales

tesis Acceso Abierto

Agregar a Mi catálogo

Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT

Autores/as: Pablo Daniel Ponzio ; Nazareno Matías Aguirre ; Carlos Gustavo López Pombo

Disponibilidad

Institución detectada	Año de publicación	Navegá	Descargá	Solicitá
No requiere	2014	Biblioteca Digital (FCEN-UBA) (SNRD)

Resumen disponible

Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariante de una estructuras de datos- las cotas ajustadas para los campos del heap son el conjunto de los valores que pueden tomar los campos en alguna instancia válida. Así, los valores de campos que no pertenecen a las cotas ajustadas pueden ser ignorados por los análisis automáticos (acotados) de código, reduciendo así el espacio de estados a explorar, y mejorando la performance del análisis. Sin embargo, el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computa estas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requiere de un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadas en entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques para resolver este problema. El primero, denominado bottom-up, utiliza un procedimiento de decisión basado en SAT para visitar instancias válidas del heap, y computa cotas ajustadas usando los valores de los campos de estas instancias. bottom-up, al igual que TACO+, requiere de una especificación en algún lenguaje declarativo de alto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera, bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, se basa en una especificación del heap en términos de un predicado inductivo de la lógica de separación. Este enfoque computa cotas ajustadas mientras realiza (un número finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnica relacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial, bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado), y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, se evaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la veri ficación de código y en la generación exhaustiva de estructuras (que satisfacen un predicado) basados en SAT. Los resultados indican que los enfoques que computan cotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechan durante el análisis, son significativamente más eficientes que los análisis convencionales, que no explotan la idea de cotas ajustadas. Además, para los análisis basados en SAT mencionados, los resultados muestran que las cotas ajustadas computadas por SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.

libros Acceso Abierto

Agregar a Mi catálogo