Deductive Software Verification -- The KeY Book : (Record no. 645077)

MARC details
000 -LEADER
fixed length control field 05964cam a2200961 c 4500
001 - CONTROL NUMBER
control field ocn968301788
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20250703165437.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS
fixed length control field m o d
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr |||||||||||
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 170113s2016 sz a o 000 0 eng d
040 ## - CATALOGING SOURCE
Original cataloging agency DKDLA
Language of cataloging eng
Description conventions pn
Transcribing agency DKDLA
Modifying agency OCLCO
-- GW5XE
-- YDX
-- UPM
-- OCLCF
-- UAB
-- COO
-- OCLCQ
-- OCLCO
-- STF
-- IOG
-- VT2
-- ESU
-- IAD
-- JBG
-- ICW
-- ILO
-- ICN
-- OTZ
-- OHI
-- OCLCQ
-- OCLCO
-- U3W
-- REB
-- CAUOI
-- JG0
-- KSU
-- UCW
-- TFW
-- OCLCQ
-- OCLCO
-- EBLCP
-- WYU
-- OCLCQ
-- ERF
-- OCLCQ
-- UBY
-- OCLCQ
-- VLB
-- OCLCQ
-- OCLCO
-- UKAHL
-- OCLCO
-- OCLCQ
-- OCL
-- OCLCO
-- OCLCL
-- SXB
-- OCLCQ
-- OCLCO
019 ## -
-- 971056996
-- 974365874
-- 981110823
-- 1005773866
-- 1012071013
-- 1026462867
-- 1048232076
-- 1049848519
-- 1066608321
-- 1081280667
-- 1086462131
-- 1112594805
-- 1132433276
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783319498126
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3319498126
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3319498118
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783319498119
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Canceled/invalid ISBN 9783319498119
Qualifying information (print)
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/978-3-319-49812-6
Source of number or code doi
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000059567500
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)968301788
Canceled/invalid control number (OCoLC)971056996
-- (OCoLC)974365874
-- (OCoLC)981110823
-- (OCoLC)1005773866
-- (OCoLC)1012071013
-- (OCoLC)1026462867
-- (OCoLC)1048232076
-- (OCoLC)1049848519
-- (OCoLC)1066608321
-- (OCoLC)1081280667
-- (OCoLC)1086462131
-- (OCoLC)1112594805
-- (OCoLC)1132433276
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.76.V47
072 #7 - SUBJECT CATEGORY CODE
Subject category code UMZ
Source bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code COM051230
Source bisacsh
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 005.1
Edition number 23
049 ## - LOCAL HOLDINGS (OCLC)
Holding library MAIN
245 00 - TITLE STATEMENT
Title Deductive Software Verification -- The KeY Book :
Remainder of title From Theory to Practice /
Statement of responsibility, etc. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hahnle, Peter H. Schmitt, Mattias Ulbrich (eds.).
264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE
Place of production, publication, distribution, manufacture Cham :
Name of producer, publisher, distributor, manufacturer Springer,
Date of production, publication, distribution, manufacture, or copyright notice 2016
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (XXXII, 702 pages) :
Other physical details illustrations
336 ## - CONTENT TYPE
Content type term text
Content type code txt
Source rdacontent
337 ## - MEDIA TYPE
Media type term computer
Media type code c
Source rdamedia
338 ## - CARRIER TYPE
Carrier type term online resource
Carrier type code cr
Source rdacarrier
347 ## - DIGITAL FILE CHARACTERISTICS
File type text file
347 ## - DIGITAL FILE CHARACTERISTICS
Encoding format PDF
490 1# - SERIES STATEMENT
Series statement Lecture Notes in Computer Science,
International Standard Serial Number 0302-9743 ;
Volume/sequential designation 10001
490 1# - SERIES STATEMENT
Series statement LNCS sublibrary. SL 2, Programming and software engineering
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Foundations -- Specification and Verification -- From Verification to Analysis -- The KeY System in Action -- Case Studies
520 8# - SUMMARY, ETC.
Summary, etc. Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of - mostly fully automated - analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework KeY. This book is the definitive guide to KeY that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind KeY for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using KeY that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M. Sc. level and beyond). The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Verification.
9 (RLIN) 1930
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer science.
9 (RLIN) 941
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Software engineering.
9 (RLIN) 14736
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Programming languages (Electronic computers)
9 (RLIN) 986
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer logic.
9 (RLIN) 6177
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logic, Symbolic and mathematical.
9 (RLIN) 1341
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Artificial intelligence.
9 (RLIN) 1340
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer programs
General subdivision Verification.
9 (RLIN) 17233
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Electronic data processing.
9 (RLIN) 6665
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logiciels
General subdivision Vérification.
9 (RLIN) 20690
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Informatique.
9 (RLIN) 14930
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Génie logiciel.
9 (RLIN) 19335
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logique informatique.
9 (RLIN) 19533
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logique symbolique et mathématique.
9 (RLIN) 11864
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Intelligence artificielle.
9 (RLIN) 15884
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element computer science.
Source of heading or term aat
9 (RLIN) 941
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element data processing.
Source of heading or term aat
9 (RLIN) 14620
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element artificial intelligence.
Source of heading or term aat
9 (RLIN) 1340
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Electronic data processing
Source of heading or term fast
9 (RLIN) 6665
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer programs
General subdivision Verification
Source of heading or term fast
9 (RLIN) 17233
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Artificial intelligence
Source of heading or term fast
9 (RLIN) 1340
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer logic
Source of heading or term fast
9 (RLIN) 6177
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer science
Source of heading or term fast
9 (RLIN) 941
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Verification
Source of heading or term fast
9 (RLIN) 1930
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logic, Symbolic and mathematical
Source of heading or term fast
9 (RLIN) 1341
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Programming languages (Electronic computers)
Source of heading or term fast
9 (RLIN) 986
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Software engineering
Source of heading or term fast
9 (RLIN) 14736
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Ahrendt, Wolfgang,
Relator term editor.
-- https://id.oclc.org/worldcat/entity/E39PCjJg7MMTDB4ggGVbQd7yV3
9 (RLIN) 59674
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Beckert, Bernhard,
Relator term editor.
-- https://id.oclc.org/worldcat/entity/E39PBJmP9pygvK3HhbJyXydxXd
9 (RLIN) 25348
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Bubel, Richard,
Relator term editor
9 (RLIN) 59675
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Hähnle, Reiner,
Relator term editor.
-- https://id.oclc.org/worldcat/entity/E39PBJhMqGBPqXDyqFfpHjwt8C
9 (RLIN) 25349
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Schmitt, P. H.
Fuller form of name (Peter H.),
Dates associated with a name 1948-
Relator term editor.
-- https://id.oclc.org/worldcat/entity/E39PBJjhD3c44V39xckh6W8wG3
9 (RLIN) 30124
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Ulbrich, Mattias,
Relator term editor
9 (RLIN) 59676
758 ## -
-- has work:
-- Deductive Software Verification -- The KeY Book (Text)
-- https://id.oclc.org/worldcat/entity/E39PCGphpdFTjjVbTRYMrHCdBd
-- https://id.oclc.org/worldcat/ontology/hasWork
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783319498119
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science ;
Volume number/sequential designation 10001,
International Standard Serial Number 0302-9743
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title LNCS sublibrary.
Number of part/section of a work SL 2,
Name of part/section of a work Programming and software engineering.
9 (RLIN) 20654
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://link.springer.com/10.1007/978-3-319-49812-6">https://link.springer.com/10.1007/978-3-319-49812-6</a>
936 ## - OCLC/CONSER MISCELLANEOUS DATA (OCLC); PIECE USED FOR CATALOGING (pre-AACR2) (RLIN)
OCLC control number(s) of parallel record(s) (OCLC); Piece used for cataloging, PUC (RLIN) BATCHLOAD
938 ## -
-- Askews and Holts Library Services
-- ASKH
-- AH34381010
938 ## -
-- ProQuest Ebook Central
-- EBLB
-- EBL6294738
938 ## -
-- ProQuest Ebook Central
-- EBLB
-- EBL5576381
938 ## -
-- YBP Library Services
-- YANK
-- 13321475
994 ## -
-- 92
-- ATIST
Holdings
Withdrawn status Lost status Damaged status Not for loan Collection code Home library Current library Date acquired Total Checkouts Date last seen Price effective from Koha item type
  Not Lost     eBook LNCS e-Library e-Library 29/07/2022   29/07/2022 29/07/2022 eBook

Powered by Koha