Automated Verification of Concurrent Search Structures (Record no. 387861)

MARC details
000 -CABECERA
campo de control de longitud fija 03557nam a22004455i 4500
001 - NÚMERO DE CONTROL
campo de control 387861
003 - IDENTIFICADOR DEL NÚMERO DE CONTROL
campo de control ES-MaUEC
005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN
campo de control 20230425112432.0
006 - CÓDIGOS DE INFORMACIÓN DE LONGITUD FIJA--CARACTERÍSTICAS DEL MATERIAL ADICIONAL
campo de control de longitud fija a||||fo|||| 00| 0
007 - CAMPO FIJO DE DESCRIPCIÓN FÍSICA--INFORMACIÓN GENERAL
campo de control de longitud fija cr nn 008mamaa
008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL
campo de control de longitud fija 230425s2021 sz | s |||| 0|eng d
020 ## - NÚMERO INTERNACIONAL ESTÁNDAR DEL LIBRO
Número Internacional Estándar del Libro 9783031018060
024 7# - IDENTIFICADOR DE OTROS ESTÁNDARES
Número estándar o código 10.1007/978-3-031-01806-0
Fuente del número o código doi
040 ## - FUENTE DE LA CATALOGACIÓN
Centro catalogador/agencia de origen ES-MaUEC
Lengua de catalogación spa
Centro/agencia transcriptor ES-MaUEC
Centro/agencia modificador ES-MaUEC
050 #4 - SIGNATURA TOPOGRÁFICA DE LA BIBLIOTECA DEL CONGRESO
Número de clasificación QA76.9.D3
Número de documento/Ítem 2021 EB
100 1# - ENTRADA PRINCIPAL--NOMBRE DE PERSONA
Nombre de persona Krishna, Siddharth
Término indicativo de función/relación autor
Código de función/relación aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 688247
245 10 - MENCIÓN DE TÍTULO
Título Automated Verification of Concurrent Search Structures
Mención de responsabilidad, etc. by Krishna Siddharth, Patel Nisarg, Shasha Dennis, Wies Thomas
250 ## - MENCIÓN DE EDICIÓN
Mención de edición 1st edition 2021
264 #1 - PRODUCCIÓN, PUBLICACIÓN, DISTRIBUCIÓN, FABRICACIÓN Y COPYRIGHT
Producción, publicación, distribución, fabricación y copyright Cham
Nombre del de productor, editor, distribuidor, fabricante Springer International Publishing
Fecha de producción, publicación, distribución, fabricación o copyright 2021
300 ## - DESCRIPCIÓN FÍSICA
Extensión 1 recurso en línea (X, 182 páginas)
336 ## - TIPO DE CONTENIDO
Término de tipo de contenido texto
Código de tipo de contenido txt
Fuente rdacontent
337 ## - TIPO DE MEDIO
Nombre/término del tipo de medio electrónico
Código del tipo de medio c
Fuente rdamedia
338 ## - TIPO DE SOPORTE
Nombre/término del tipo de soporte recurso electrónico
Código del tipo de soporte cr
Fuente rdacarrier
347 ## - CARACTERÍSTICAS DEL ARCHIVO DIGITAL
Tipo de archivo archivo de texto
Formato de codificación PDF
490 0# - MENCIÓN DE SERIE
Mención de serie Synthesis Lectures on Computer Science
Número Internacional Normalizado para Publicaciones Seriadas 1932-1686
505 0# - NOTA DE CONTENIDO CON FORMATO
Nota de contenido con formato Acknowledgments -- Introduction -- Preliminaries -- Separation Logic -- Ghost State -- The Keyset Resource Algebra -- The Edgeset Framework for Single-Copy Structures -- The Flow Framework -- Verifying Single-Copy Concurrent Search Structures -- Verifying Multicopy Structures -- The Edgeset Framework for Multicopy Structures -- Reasoning about Non-Static and Non-Local Linearization Points -- Verifying the LSM DAG Template -- Proof Mechanization and Automation -- Related Work, Future Work, and Conclusion -- Bibliography -- Authors' Biographies.
520 ## - SUMARIO, ETC.
Sumario, etc. Search structures support the fundamental data storage primitives on key-value pairs: insert a pair, delete by key, search by key, and update the value associated with a key. Concurrent search structures are parallel algorithms to speed access to search structures on multicore and distributed servers. These sophisticated algorithms perform fine-grained synchronization between threads, making them notoriously difficult to design correctly. Indeed, bugs have been found both in actual implementations and in the designs proposed by experts in peer-reviewed publications. The rapid development and deployment of these concurrent algorithms has resulted in a rift between the algorithms that can be verified by the state-of-the-art techniques and those being developed and used today. The goal of this book is to show how to bridge this gap in order to bring the certified safety of formal verification to high-performance concurrent search structures. Similar techniques and frameworks can be applied to concurrent graph and network algorithms beyond search structures.
988 ## - NOTA LOCAL 598
Nota local 598 (boletines) Synthesis Collection of Technology_2021
650 #7 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA
Fuente del encabezamiento o término embne
9 (RLIN) 151535
Término de materia o nombre geográfico como elemento de entrada Estructuras de datos (Informática)
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Patel, Nisarg
Término indicativo de función/relación autor
Código de función/relación aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 688248
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Shasha, Dennis Elliott
Término indicativo de función/relación autor
Código de función/relación aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 686965
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Wies, Thomas
Término indicativo de función/relación autor
Código de función/relación aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 688249
776 08 - ENTRADA/ENLACE A UN FORMATO FÍSICO ADICIONAL
Información de relación/Frase instructiva de referencia Printed edition:
Número Internacional Estándar del Libro 9783031000744
776 08 - ENTRADA/ENLACE A UN FORMATO FÍSICO ADICIONAL
Información de relación/Frase instructiva de referencia Printed edition:
Número Internacional Estándar del Libro 9783031006784
776 08 - ENTRADA/ENLACE A UN FORMATO FÍSICO ADICIONAL
Información de relación/Frase instructiva de referencia Printed edition:
Número Internacional Estándar del Libro 9783031029349
856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS
Identificador Uniforme del Recurso https://go.openathens.net/redirector/universidadeuropea.es?url=https://doi.org/10.1007/978-3-031-01806-0
Nota pública Acceso a este recurso digital (usuarios Universidad Europea de Madrid)
942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA)
Fuente del sistema de clasificación o colocación Library of Congress Classification
Tipo de ítem Koha LIBRO-E NO PRÉSTAMO
998 ## - DATOS ESTADÍSTICOS
Fecha de catalogación
Tipo de materia E-book
Catalogador Irene González
Catalogado
Holdings
Información adicional para el OPAC Código 2 (categoría) Estado de pérdida Fuente del sistema de clasificación o colocación Tipo de material Código 1: Estado físico No se presta Código de colección Estado Localización permanente Ubicación/localización actual Ubicación en estantería Fecha de adquisición Tipo de préstamo Total de préstamos Signatura topográfica completa Código de barras Fecha visto por última vez Precio válido a partir de Tipo de ítem Koha
Acceso concurrente No retirado   Library of Congress Classification E-Libro Buen estado Acceso electrónico Ciencias e Ingeniería Acceso electrónico Madrid Digital Madrid Digital Acceso Electrónico (UEM) 25/11/2022 En línea   QA76.9.D3 2021 EB eBook.01113060 25/11/2022 25/11/2022 LIBRO-E NO PRÉSTAMO