UNIGE document Master
previous document  unige:15811  next document
add to browser collection

Built-in support for Abstract Data Types in the Σ Decision Diagram framework

Defense Maîtrise : Univ. Genève, 2010
Abstract Encoding and rewriting of large sets of terms is very useful in different do- mains such as model checking and theorem proving. Σ Decision Diagrams (ΣDD) have been developed to encode and rewrite large sets of terms in efficient manner, both in terms of space and memory. ΣDD encode terms in a symbolic and canonical way to ensure the sharing of redundant terms and subterms and also to be able to apply rewriting rules. In certain cases however the computer's built-in implementation might be faster than the symbolic approach. In this thesis we first extend the ΣDDs definition in or- der to support built-in types. Afterwards we extend the ΣDDs set operations to handle the extended ΣDD. Then, we modify the rewriting mechanism in order to perform built-in operations on the extended ΣDD by bypassing the normal mechanism and using the computer built-in mechanisms. Finally, we show that the new approach is much faster than the previous one in almost all different cases.
Keywords ∑DDDecision diagramTerm rewritingSymbolic techniquesSet of terms
Full text
Master (760 Kb) - document accessible for UNIGE members only Limited access to UNIGE
Research group Software Modeling and Verification
(ISO format)
LOPEZ BOBEDA, Edmundo. Built-in support for Abstract Data Types in the Σ Decision Diagram framework. Université de Genève. Maîtrise, 2010. https://archive-ouverte.unige.ch/unige:15811

115 hits



Deposited on : 2011-05-13

Export document
Format :
Citation style :