Please use this identifier to cite or link to this item:
|Title:||Computer Aided Verification of Relational Models by Strategic Rewriting|
José Nuno Oliveira
|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.|
|Appears in Collections:||HASLab - Articles in International Journals|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.