Computer Aided Verification of Relational Models

Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such a...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Necco, Claudia Mónica, Oliveira, José R., Visser, Joost, Uzal, Roberto
Formato:	Objeto de conferencia
Lenguaje:	Inglés
Publicado:	2016
Materias:	Ciencias Informáticas models verification symbolic execution extended static checking strategic term rewriting
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/56730
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-56730
record_format	dspace
institution	Universidad Nacional de La Plata
institution_str	I-19
repository_str	R-120
collection	SEDICI (UNLP)
language	Inglés
topic	Ciencias Informáticas models verification symbolic execution extended static checking strategic term rewriting
spellingShingle	Ciencias Informáticas models verification symbolic execution extended static checking strategic term rewriting Necco, Claudia Mónica Oliveira, José R. Visser, Joost Uzal, Roberto Computer Aided Verification of Relational Models
topic_facet	Ciencias Informáticas models verification symbolic execution extended static checking strategic term rewriting
description	Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions.We developed a type-directed, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.
format	Objeto de conferencia Objeto de conferencia
author	Necco, Claudia Mónica Oliveira, José R. Visser, Joost Uzal, Roberto
author_facet	Necco, Claudia Mónica Oliveira, José R. Visser, Joost Uzal, Roberto
author_sort	Necco, Claudia Mónica
title	Computer Aided Verification of Relational Models
title_short	Computer Aided Verification of Relational Models
title_full	Computer Aided Verification of Relational Models
title_fullStr	Computer Aided Verification of Relational Models
title_full_unstemmed	Computer Aided Verification of Relational Models
title_sort	computer aided verification of relational models
publishDate	2016
url	http://sedici.unlp.edu.ar/handle/10915/56730
work_keys_str_mv	AT neccoclaudiamonica computeraidedverificationofrelationalmodels AT oliveirajoser computeraidedverificationofrelationalmodels AT visserjoost computeraidedverificationofrelationalmodels AT uzalroberto computeraidedverificationofrelationalmodels
bdutipo_str	Repositorios
_version_	1764820477540302848

Computer Aided Verification of Relational Models

Ejemplares similares