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
Stable URL https://archive-ouverte.unige.ch/unige:15811
Full text
Master (760 Kb) - document accessible for UNIGE members only Limited access to UNIGE
Research group Software Modeling and Verification

113 hits



Deposited on : 2011-05-13

Export document
Format :
Citation style :