CATÁLOGO DE LA BIBLIOTECA DE LA FaMAF
Normal view MARC view ISBD view

Implementación del algoritmo Gauss-Seidel en CUDA para la verificación simbólica de modelos probabilísticos / Gastón Ingaramo.

By: Ingaramo, Gastón, 1988-.
Contributor(s): D'Argenio, Pedro Ruben, 1968- [dir.].
Material type: materialTypeLabelBookPublisher: [S.l. : s.n. ], 2013Description: v, 89 p. : il. (algunas col.) ; 30 cm.Subject(s): Software -- program verification | Concurrent programming | Numerical analysis | Sistemas de ecuaciones lineales | Model checking | Computación de alta performance | Modelos probabilistasOnline resources: Acceso a Versión Digital. Disponible en línea.Dissertation note: Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2013. Summary: Presentamos los distintos lenguajes para el modelado de sistemas, tanto de tiempo discreto como de tiempo continuo, DTMC y CTMC respectivamente. Luego estudiamos las lógicas correspondientes para su verificación prestando especial atención a los operadores que requieren de multiplicaciones matriz-vector. Explicamos como PRISM, el model checker simbólico utilizado, implementa estos operadores y que estructuras de datos utiliza. Finalmente presentamos nuestra implementación de un algoritmo pseudo Gauss- Seidel en arquitecturas GPGPU, principalmente en CUDA. Hacemos dos distinciones, cuando la memoria de la tarjeta es suciente para contener todos los vectores y cuando se requiere dividir el problema. Concluímos con un análisis experimental que demuestra las mejoras del desempeño obtenidas.
Tags from this library: No tags from this library for this title. Log in to add tags.
Item type Current location Call number URL Copy number Status Notes Date due Barcode Item holds
Trabajo Especial de Grado Trabajo Especial de Grado FaMAF
Secc. Tesis y Trabajos especiales
TE C ING http://www.famaf.unc.edu.ar/institucional/biblioteca/trabajos/638/16932.pdf 1 Available Disponible también en línea. 22023
Total holds: 0

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2013.

Incluye referencias bibliográficas : p. 88-89.

Presentamos los distintos lenguajes para el modelado de sistemas, tanto de tiempo discreto como de tiempo continuo, DTMC y CTMC respectivamente. Luego estudiamos las lógicas correspondientes para su verificación prestando especial atención a los operadores que requieren de multiplicaciones matriz-vector. Explicamos como PRISM, el model checker
simbólico utilizado, implementa estos operadores y que estructuras de datos utiliza.
Finalmente presentamos nuestra implementación de un algoritmo pseudo Gauss- Seidel en arquitecturas GPGPU, principalmente en CUDA. Hacemos dos distinciones,
cuando la memoria de la tarjeta es suciente para contener todos los vectores y cuando se requiere dividir el problema. Concluímos con un análisis experimental que demuestra
las mejoras del desempeño obtenidas.

Disponible en línea.

La biblioteca posee 1 ej.

Click on an image to view it in the image viewer

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:00hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127(Atención al Público) int. 41151(Dirección)

biblio@famaf.unc.edu.ar

publicofamaf@gmail.com



//