Computer Aided Verification of Relational Models by Strategic Rewriting

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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Necco, Claudia Mónica, Oliveira, José N., Visser, Joost, Uzal, Roberto
Formato:	Articulo
Lenguaje:	Inglés
Publicado:	2017
Materias:	Ciencias Informáticas models verification symbolic execution abstract model verification extended static checking strategic term rewriting
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/62942 http://journal.info.unlp.edu.ar/wp-content/uploads/2017/10/JCST-45-Paper-7.pdf
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-62942
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 abstract model verification extended static checking strategic term rewriting
spellingShingle	Ciencias Informáticas models verification symbolic execution abstract model verification extended static checking strategic term rewriting Necco, Claudia Mónica Oliveira, José N. Visser, Joost Uzal, Roberto Computer Aided Verification of Relational Models by Strategic Rewriting
topic_facet	Ciencias Informáticas models verification symbolic execution abstract model verification 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 typedirected, 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	Articulo Articulo
author	Necco, Claudia Mónica Oliveira, José N. Visser, Joost Uzal, Roberto
author_facet	Necco, Claudia Mónica Oliveira, José N. Visser, Joost Uzal, Roberto
author_sort	Necco, Claudia Mónica
title	Computer Aided Verification of Relational Models by Strategic Rewriting
title_short	Computer Aided Verification of Relational Models by Strategic Rewriting
title_full	Computer Aided Verification of Relational Models by Strategic Rewriting
title_fullStr	Computer Aided Verification of Relational Models by Strategic Rewriting
title_full_unstemmed	Computer Aided Verification of Relational Models by Strategic Rewriting
title_sort	computer aided verification of relational models by strategic rewriting
publishDate	2017
url	http://sedici.unlp.edu.ar/handle/10915/62942 http://journal.info.unlp.edu.ar/wp-content/uploads/2017/10/JCST-45-Paper-7.pdf
work_keys_str_mv	AT neccoclaudiamonica computeraidedverificationofrelationalmodelsbystrategicrewriting AT oliveirajosen computeraidedverificationofrelationalmodelsbystrategicrewriting AT visserjoost computeraidedverificationofrelationalmodelsbystrategicrewriting AT uzalroberto computeraidedverificationofrelationalmodelsbystrategicrewriting
bdutipo_str	Repositorios
_version_	1764820480173277188

Computer Aided Verification of Relational Models by Strategic Rewriting

Ejemplares similares