Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/10531
Title: Computer Aided Verification of Relational Models by Strategic Rewriting
Authors: Visser,J
Uzal,R
Necco,CM
José Nuno Oliveira
Issue Date: 2017
Abstract: 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.
URI: http://repositorio.inesctec.pt/handle/123456789/10531
metadata.dc.type: Publication
article
Appears in Collections:HASLab - Articles in International Journals

Files in This Item:
File Description SizeFormat 
P-00N-KTV.pdf986.5 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.