Navegación

Búsqueda

Búsqueda avanzada

Resultados de búsqueda para Data Structures

Semantrix: A Compressed Semantic Matrix

We present a compact data structure to represent both the duration and length of homogeneous segments of trajectories from moving objects in a way that, as a data warehouse, it allows us to efficiently answer cumulative queries. The division of trajectories into relevant segments has been studied in the literature under the topic of Trajectory Segmentation. In this paper, we design a data structure to compactly represent them and the algorithms to answer the more relevant queries. We experimentally evaluate our proposal in the real context of an enterprise with mobile workers (truck drivers) where we aim at analyzing the time they spend in different activities. To test our proposal under higher stress conditions we generated a huge amount of synthetic realistic trajectories and evaluated our system with those data to have a good idea about its space needs and its efficiency when answering different types of queries.

Autores: Nieves R. Brisaboa / Antonio Fariña / Gonzalo Navarro / Tirso V. Rodeiro / 
Palabras Clave: Aggregation - Data Structures - Multidimensional data

Verification of mutable data structures in Dafny: methodological aspects

We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny. In particular, we devise a generic verification methodology and apply it to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The layered approach presented in this paper allows us to progressively refine some aspects of the specification, such as iterator invalidation. We also introduce a stratified view of the footprint of an instance (i.e. the set of memory locations owned by that instance), and identify the boilerplate conditions common to all operations of an ADT. We also show the usage of the resulting implementations by means of verified examples.

Autores: Jorge Blázquez / Manuel Montenegro / Clara Segura / 
Palabras Clave: abstract data types - Dafny - Data Structures - program verification

An Exercise in Proving Red-Black Trees Correct (Trabajo en progreso)

Red-black trees are an efficient data structure that constitutes the basis for implementing maps, multimaps, sets and multisets, in the standard libraries of many programming languages. It achieves logarithmic costs for searching, inserting, and deleting keys, but keeping them balanced frequently requires to deal with a high number of cases. However, a variant called «Left-Leaning», due to Robert Sedgewick, reduces the number of cases to a few ones. We present here a functional version of these red-black trees and prove them correct with respect to a model-based specification, being the model of a red-black tree a set of elements. We have used the Dafny verification platform, which provides the programming language, the assertion language, and the verifier. The latter is an up-to-date SMT solver (Satisfiability Modulo Theories), which can deal with a rather large decidable fragment of the first-order logic.

Autores: Ricardo Peña / 
Palabras Clave: Balanced Trees - Data Structures - Formal Verification - verification platforms

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada