Generación de invariantes para implementar eficientemente regiones críticas condicionales

La técnica de semáforos binarios divididos (SBS) puede ser usada para implementar regiones críticas condicionales. Dada una especificación de un problema de esta clase. SBS brinda tanto los programas que lo implementan como los invariantes que aseguran su corrección. Aplicando la técnica a casos par...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Barsotti, Damián, Blanco, Javier
Formato:	Objeto de conferencia
Lenguaje:	Español
Publicado:	2007
Materias:	Ciencias Informáticas Informática Concurrent Programming semáforos binarios divididos Automatic Programming
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/23279
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-23279
record_format	dspace
institution	Universidad Nacional de La Plata
institution_str	I-19
repository_str	R-120
collection	SEDICI (UNLP)
language	Español
topic	Ciencias Informáticas Informática Concurrent Programming semáforos binarios divididos Automatic Programming
spellingShingle	Ciencias Informáticas Informática Concurrent Programming semáforos binarios divididos Automatic Programming Barsotti, Damián Blanco, Javier Generación de invariantes para implementar eficientemente regiones críticas condicionales
topic_facet	Ciencias Informáticas Informática Concurrent Programming semáforos binarios divididos Automatic Programming
description	La técnica de semáforos binarios divididos (SBS) puede ser usada para implementar regiones críticas condicionales. Dada una especificación de un problema de esta clase. SBS brinda tanto los programas que lo implementan como los invariantes que aseguran su corrección. Aplicando la técnica a casos particulares se encuentran programas que admiten simplificaciones. Este trabajo se concentra en el desarrollo de un sistema automático para obtener estas simplificaciones. El procedimiento consiste en hacer una búsqueda de nuevos invariantes que avalen la corrección de las simplificaciones. Para esto usamos técnicas de generación de invariantes, en particular propagación hacia los más débiles. Su implementación fue realizada usando los demostradores Isabelle /HOL v CVC Lite para las demostraciones de validez y simplificaciones de las formulas lógicas envueltas en el proceso. El método fue probado sobre diferentes ejemplos clásicos de programación concurrente.
format	Objeto de conferencia Objeto de conferencia
author	Barsotti, Damián Blanco, Javier
author_facet	Barsotti, Damián Blanco, Javier
author_sort	Barsotti, Damián
title	Generación de invariantes para implementar eficientemente regiones críticas condicionales
title_short	Generación de invariantes para implementar eficientemente regiones críticas condicionales
title_full	Generación de invariantes para implementar eficientemente regiones críticas condicionales
title_fullStr	Generación de invariantes para implementar eficientemente regiones críticas condicionales
title_full_unstemmed	Generación de invariantes para implementar eficientemente regiones críticas condicionales
title_sort	generación de invariantes para implementar eficientemente regiones críticas condicionales
publishDate	2007
url	http://sedici.unlp.edu.ar/handle/10915/23279
work_keys_str_mv	AT barsottidamian generaciondeinvariantesparaimplementareficientementeregionescriticascondicionales AT blancojavier generaciondeinvariantesparaimplementareficientementeregionescriticascondicionales
bdutipo_str	Repositorios
_version_	1764820466069929986

Generación de invariantes para implementar eficientemente regiones críticas condicionales

Ejemplares similares