Master
English

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

Defense date2010
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
  • ∑DD
  • Decision diagram
  • Term rewriting
  • Symbolic techniques
  • Set of terms
Citation (ISO format)
LOPEZ BOBEDA, Edmundo. Built-in support for Abstract Data Types in the Σ Decision Diagram framework. Master, 2010.
Main files (1)
Master thesis
accessLevelRestricted
Identifiers
  • PID : unige:15811
184views
1downloads

Technical informations

Creation14/12/2010 17:28:00
First validation14/12/2010 17:28:00
Update time14/03/2023 16:51:34
Status update14/03/2023 16:51:34
Last indexation29/10/2024 18:07:02
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack