Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings /
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Format: | Conference Proceeding Book |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
c2003
Berlin ; New York : Springer-Verlag, ©2003 Berlin ; New York : c2003 New York : 2003 Berlin ; New York : [2003] |
| Series: | Lecture notes in computer science ;
2860 Lecture notes in computer science ; 2860 Lecture notes in computer science 2860 Lecture notes in computer science 2860 |
| Subjects: |
| LEADER | 18467nam a2201705 a 4500 | ||
|---|---|---|---|
| 001 | 3bec4f87-567f-4c80-a602-db7f2a1685db | ||
| 005 | 20240310000000.0 | ||
| 008 | 031001s2003 nyua b 001 0 eng | ||
| 010 | |a 2003057017 | ||
| 010 | |a 2003057017 | ||
| 015 | |a 03,N44,0228 |2 dnb | ||
| 015 | |a GBA3-76810 | ||
| 015 | |a GBA376810 |2 bnb | ||
| 016 | 7 | |a 009728090 |2 Uk | |
| 016 | 7 | |a 968923445 |2 DE-101 | |
| 016 | 7 | |a 968923445 |2 GyFmDB | |
| 019 | |a 53436841 |a 456807478 |a 960143205 |a 1071574037 | ||
| 020 | |a 354020363X (alk. paper) | ||
| 020 | |a 354020363X |q (alk. paper) | ||
| 020 | |a 354020363X |q (alkaline paper) | ||
| 020 | |a 354020363X |q alkaline paper | ||
| 020 | |a 9783540203636 |q (alk. paper) | ||
| 020 | |a 9783540203636 |q (alkaline paper) | ||
| 024 | 3 | |a 9783540203636 | |
| 035 | |a (CStRLIN)XBCP2003057017-B | ||
| 035 | |a (CtY)6424925 | ||
| 035 | |a (DLC) 2003057017 | ||
| 035 | |a (NNC)4199214 | ||
| 035 | |a (OCoLC)53170443 |z (OCoLC)53436841 |z (OCoLC)456807478 |z (OCoLC)960143205 |z (OCoLC)1071574037 | ||
| 035 | |a (OCoLC)53170443 | ||
| 035 | |a (OCoLC)ocm53170443 |9 ExL | ||
| 035 | |a (OCoLC)ocm53170443 | ||
| 035 | |a (OCoLC)ocn691031301 | ||
| 035 | |a (PU)3505615-penndb-Voyager | ||
| 035 | |a (RPB)b34895395-01bu_inst | ||
| 035 | |a 3505615 | ||
| 035 | |a 4001338 | ||
| 035 | |a 4199214 | ||
| 035 | |a 4993882 | ||
| 035 | |a 53170443 | ||
| 035 | |a 6424925 | ||
| 035 | |a CTYA6424925-B | ||
| 040 | |a DLC |b eng |c DLC |d OHX |d UKM |d C$Q |d IXA |d BAKER |d NLGGC |d BTCTA |d YDXCP |d LVB |d UQ1 |d OCLCG |d IG# |d STF |d DEBBG |d CEF |d ILU |d OCLCF |d OCLCQ |d OCLCO |d QE2 |d BDX |d UKMGB |d OCL |d OCLCO |d DEBSZ |d CAUOI |d OCLCO |d OCLCA |d OCLCQ |d UWO |d OCLCQ | ||
| 040 | |a DLC |b eng |c DLC |d OHX |d UKM |d CQ |d IXA |d BAKER |d NLGGC |d BTCTA |d YDXCP |d LVB |d UQ1 |d OCLCG |d IG# |d STF |d DEBBG |d CEF |d ILU |d OCLCF |d OCLCQ |d OCLCO |d QE2 |d BDX |d UKMGB |d OCL |d OCLCO |d DEBSZ |d CAUOI |d OCLCO |d OCLCA |d OCLCQ |d UWO |d OCLCQ |d IL4J6 | ||
| 040 | |a DLC |b eng |c DLC |d OrLoB | ||
| 040 | |a DLC |c DLC |d CtY | ||
| 040 | |a DLC |c DLC |d OHX |d OCoLC |d OrLoB-B | ||
| 040 | |a DLC |c DLC |d OHX |d OrLoB-B | ||
| 040 | |a DLC |c DLC |d OHX |d UKM |d OCLCQ |d RBN | ||
| 042 | |a pcc | ||
| 049 | |a CGUA | ||
| 049 | |a RBNN | ||
| 050 | 0 | 0 | |a TK7874.75 |b .C453 2003 |
| 055 | 3 | |a QA75 |b .L38 no.2860 | |
| 072 | 7 | |a TK |2 lcco | |
| 079 | |a ocm53170443 | ||
| 082 | 0 | 0 | |a 621.39/5 |2 22 |
| 084 | |a 54.20 |2 bcl | ||
| 084 | |a DAT 190f |2 stub | ||
| 084 | |a SS 4800 |2 rvk | ||
| 090 | |a TK7874.75 |b .C453 2003 | ||
| 111 | 2 | |a CHARME 2003 |d (2001 : |c L'Aquila, Italy) | |
| 111 | 2 | |a CHARME 2003 |d (2003 : |c L'Aquila, Italy) |0 http://viaf.org/viaf/sourceID/LC|n2003016857 | |
| 111 | 2 | |a CHARME 2003 |d (2003 : |c L'Aquila, Italy) |1 http://viaf.org/viaf/145616127 | |
| 111 | 2 | |a CHARME 2003 |d (2003 : |c L'Aquila, Italy) | |
| 245 | 1 | 0 | |a Correct hardware design and verification methods : |b 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings / |c Daniel Geist, Enrico Tronci, (Eds.) |
| 246 | 1 | 4 | |a IFIP/WG 10.5 |
| 246 | 1 | 8 | |a CHARME 2003 |
| 246 | 3 | 0 | |a 12th IFIP WG 10.5 Advanced Research Working Conference |
| 246 | 3 | 0 | |a CHARME 2003 |
| 260 | |a Berlin ; |a New York : |b Springer, |c c2003 | ||
| 260 | |a Berlin ; |a New York : |b Springer, |c ©2003 | ||
| 260 | |a Berlin ; |a New York : |b Springer-Verlag, |c c2003 | ||
| 260 | |a New York : |b Springer-Verlag, |c 2003 | ||
| 263 | |a 0311 | ||
| 264 | 1 | |a Berlin ; |a New York : |b Springer, |c [2003] | |
| 264 | 4 | |c ©2003 | |
| 300 | |a xii, 426 p. : |b ill. ; |c 24 cm | ||
| 300 | |a xii, 426 pages : |b illustrations ; |c 24 cm | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a unmediated |b n |2 rdamedia | ||
| 338 | |a volume |b nc |2 rdacarrier | ||
| 347 | |a text file |2 rdaft | ||
| 440 | 0 | |a Lecture notes in computer science ; |v 2860 | |
| 490 | 1 | |a Lecture notes in computer science ; |v 2860 | |
| 490 | 1 | |a Lecture notes in computer science, |x 0302-9743 ; |v 2860 | |
| 500 | |a This WorldCat-derived record is shareable under Open Data Commons ODC-BY, with attribution to OCLC |5 CTY | ||
| 504 | |a Includes bibliographical references and index | ||
| 505 | 0 | 0 | |t What Is beyond the RTL Horizon for Microprocessor and System Design? / |r Wolfgang Roesner -- |t The Charme of Abstract Entities / |r Fabio Somenzi -- |t The PSL/Sugar Specification Language: A Language for all Seasons / |r Daniel Geist -- |t Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular / |r Mary Sheeran -- |t Predicate Abstraction with Minimum Predicates / |r Sagar Chaki, Edmund Clarke, Alex Groce and Ofer Strichman -- |t Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning / |r Sharon Barner and Ishai Rabinovitz -- |t Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP / |r Sven Beyer, Chris Jacobi, Daniel Kroning, Dirk Leinenbach and Wolfgang J. Paul -- |t A Hazards-Based Correctness Statement for Pipelined Circuits / |r Mark D. Aagaard -- |t Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT / |r Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom and Konrad Slind -- |t On Complementing Nondeterministic Buchi Automata / |r Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi and Moshe Y. Vardi -- |t Coverage Metrics for Formal Verification / |r Hana Chockler, Orna Kupferman and Moshe Y. Vardi -- |t "More Deterministic" vs. "Smaller" Buchi Automata for Efficient LTL Model Checking / |r Roberto Sebastiani and Stefano Tonetta -- |t An Optimized Symbolic Bounded Model Checking Engine / |r Rachel Tzoref, Mark Matusevich, Eli Berger and Ilan Beer -- |t Constrained Symbolic Simulation with Mathematica and ACL2 / |r Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier and Dominique Borrione -- |t Semi-formal Verification of Memory Systems by Symbolic Simulation / |r Husam Abu-Haimed, Sergey Berezin and David L. Dill -- |t CTL May be Ambiguous When Model Checking Moore Machines / |r Cedric Roux and Emmanuelle Encrenaz -- |t Reasoning about GSTE Assertion Graphs / |r Alan J. Hu, Jeremy Casas and Jin Yang -- |t Towards Diagrammability and Efficiency in Event Sequence Languages / |r Kathi Fisler -- |t Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving / |r Mike Gordon, Joe Hurd and Konrad Slind -- |t On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking / |r E. Allen Emerson and Thomas Wahl -- |t On the Correctness of an Intrusion-Tolerant Group Communication Protocol / |r Mohamed Layouni, Jozef Hooman and Sofiene Tahar -- |t Exact and Efficient Verification of Parameterized Cache Coherence Protocols / |r E. Allen Emerson and Vineet Kahlon -- |t Design and Implementation of an Abstract Interpreter for VHDL / |r Charles Hymans -- |t A Programming Language Based Analysis of Operand Forwarding / |r Lennart Beringer -- |t Integrating RAM and Disk Based Verification within the Mur[phi] Verifier / |r Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci and Marisa Venturini Zilli -- |t Design and Verification of CoreConnectTM IP Using Esterel / |r Satnam Singh -- |t Inductive Assertions and Operational Semantics / |r J. Strother Moore -- |t A Compositional Theory of Refinement for Branching Time / |r Panagiotis Manolios -- |t Linear and Nonlinear Arithmetic in ACL2 / |r Warren A. Hunt, Jr., Robert Bellarmine Krug and J. Moore -- |t Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking / |r Malay K. Ganai, Aarti Gupta, Zijiang Yang and Pranav Ashar -- |t Convergence Testing in Term-Level Bounded Model Checking / |r Randal E. Bryant, Shuvendu K. Lahiri and Sanjit A. Seshia -- |t The ROBDD Size of Simple CNF Formulas / |r Michael Longberg, Amir Pnueli and Yoav Rodeh -- |t Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems / |r Enric Pastor and Marco A. Pena -- |t Finite Horizon Analysis of Markov Chains with the Mur[phi] Verifier / |r Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci and Marisa Venturini Zilli -- |t Improved Symbolic Verification Using Partitioning Techniques / |r Subramanian Iyer, Debashis Sahoo, Christian Stangier, Amit Narayan and Jawahar Jain |
| 505 | 0 | 0 | |t What Is beyond the RTL Horizon for Microprocessor and System Design? / |r Wolfgang Roesner -- |t The Charme of Abstract Entities / |r Fabio Somenzi -- |t The PSL/Sugar Specification Language: A Language for all Seasons / |r Daniel Geist -- |t Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular / |r Mary Sheeran -- |t Predicate Abstraction with Minimum Predicates / |r Sagar Chaki, Edmund Clarke, Alex Groce and Ofer Strichman -- |t Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning / |r Sharon Barner and Ishai Rabinovitz -- |t Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP / |r Sven Beyer, Chris Jacobi, Daniel Kroning, Dirk Leinenbach and Wolfgang J. Paul -- |t A Hazards-Based Correctness Statement for Pipelined Circuits / |r Mark D. Aagaard -- |t Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT / |r Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom and Konrad Slind -- |t On Complementing Nondeterministic Buchi Automata / |r Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi and Moshe Y. Vardi -- |t Coverage Metrics for Formal Verification / |r Hana Chockler, Orna Kupferman and Moshe Y. Vardi -- |t "More Deterministic" vs. "Smaller" Buchi Automata for Efficient LTL Model Checking / |r Roberto Sebastiani and Stefano Tonetta -- |t An Optimized Symbolic Bounded Model Checking Engine / |r Rachel Tzoref, Mark Matusevich, Eli Berger and Ilan Beer -- |t Constrained Symbolic Simulation with Mathematica and ACL2 / |r Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier and Dominique Borrione -- |t Semi-formal Verification of Memory Systems by Symbolic Simulation / |r Husam Abu-Haimed, Sergey Berezin and David L. Dill -- |t CTL May be Ambiguous When Model Checking Moore Machines / |r Cedric Roux and Emmanuelle Encrenaz -- |t Reasoning about GSTE Assertion Graphs / |r Alan J. Hu, Jeremy Casas and Jin Yang -- |t Towards Diagrammability and Efficiency in Event Sequence Languages / |r Kathi Fisler -- |t Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving / |r Mike Gordon, Joe Hurd and Konrad Slind -- |t On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking / |r E. Allen Emerson and Thomas Wahl -- |t On the Correctness of an Intrusion-Tolerant Group Communication Protocol / |r Mohamed Layouni, Jozef Hooman and Sofiene Tahar -- |t Exact and Efficient Verification of Parameterized Cache Coherence Protocols / |r E. Allen Emerson and Vineet Kahlon -- |t Design and Implementation of an Abstract Interpreter for VHDL / |r Charles Hymans -- |t A Programming Language Based Analysis of Operand Forwarding / |r Lennart Beringer -- |t Integrating RAM and Disk Based Verification within the Mur[phi] Verifier / |r Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci and Marisa Venturini Zilli -- |t Design and Verification of CoreConnectTM IP Using Esterel / |r Satnam Singh -- |t Inductive Assertions and Operational Semantics / |r J. Strother Moore -- |t A Compositional Theory of Refinement for Branching Time / |r Panagiotis Manolios -- |t Linear and Nonlinear Arithmetic in ACL2 / |r Warren A. Hunt, Jr., Robert Bellarmine Krug and J. Moore -- |t Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking / |r Malay K. Ganai, Aarti Gupta, Zijiang Yang and Pranav Ashar -- |t Convergence Testing in Term-Level Bounded Model Checking / |r Randal E. Bryant, Shuvendu K. Lahiri and Sanjit A. Seshia -- |t The ROBDD Size of Simple CNF Formulas / |r Michael Longberg, Amir Pnueli and Yoav Rodeh -- |t Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems / |r Enric Pastor and Marco A. Pena -- |t Finite Horizon Analysis of Markov Chains with the Mur[phi] Verifier / |r Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci and Marisa Venturini Zilli -- |t Improved Symbolic Verification Using Partitioning Techniques / |r Subramanian Iyer, Debashis Sahoo, Christian Stangier, Amit Narayan and Jawahar Jain |
| 505 | 0 | 0 | |t What Is beyond the RTL Horizon for Microprocessor and System Design? / |r Wolfgang Roesner -- |t The Charme of Abstract Entities / |r Fabio Somenzi -- |t The PSL/Sugar Specification Language: A Language for all Seasons / |r Daniel Geist -- |t Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular / |r Mary Sheeran -- |t Predicate Abstraction with Minimum Predicates / |r Sagar Chaki, Edmund Clarke, Alex Groce and Ofer Strichman -- |t Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning / |r Sharon Barner and Ishai Rabinovitz -- |t Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP / |r Sven Beyer, Chris Jacobi, Daniel Kroning, Dirk Leinenbach and Wolfgang J. Paul |
| 530 | |a Also available online as: Informatics (Online) | ||
| 530 | |a Also available via the World Wide Web | ||
| 650 | 0 | |a Integrated circuits |x Verification |v Congresses | |
| 650 | 0 | |a Integrated circuits |x Very large scale integration |x Computer-aided design |v Congresses | |
| 650 | 6 | |a Circuits intégrés à très grande échelle |x Conception assistée par ordinateur |v Congrès | |
| 650 | 6 | |a Circuits intégrés |x Vérification |v Congrès | |
| 650 | 7 | |a Circuit intégré à très grande échelle |2 rasuqam | |
| 650 | 7 | |a Circuit intégré |2 rasuqam | |
| 650 | 7 | |a Conception assistée par ordinateur |2 rasuqam | |
| 650 | 7 | |a Entwurfsautomation |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|043125360 | |
| 650 | 7 | |a Entwurfssprache |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|042953359 | |
| 650 | 7 | |a Formale Methode |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|940624109 | |
| 650 | 7 | |a Hardwareentwurf |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|041591038 | |
| 650 | 7 | |a Hardwareverifikation |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|042149827 | |
| 650 | 7 | |a Integrated circuits |x Verification |2 fast |0 http://id.worldcat.org/fast/fst00975600 | |
| 650 | 7 | |a Integrated circuits |x Verification |2 fast | |
| 650 | 7 | |a Integrated circuits |x Very large scale integration |x Computer-aided design |2 fast |0 http://id.worldcat.org/fast/fst00975604 | |
| 650 | 7 | |a Integrated circuits |x Very large scale integration |x Computer-aided design |2 fast | |
| 650 | 7 | |a Kongress |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|041304705 | |
| 650 | 7 | |a Model Checking |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|949342122 | |
| 650 | 7 | |a Model-checking (Informatique) |2 rasuqam | |
| 650 | 7 | |a System-on-Chip |2 gnd |0 http://viaf.org/viaf/sourceID/DNB|968378781 | |
| 650 | 7 | |a Vérification de logiciels |2 rasuqam | |
| 650 | 1 | 7 | |a Hardware |2 gtt |
| 650 | 1 | 7 | |a Vormgeving |2 gtt |
| 655 | 7 | |a Conference papers and proceedings |2 fast |0 http://id.worldcat.org/fast/fst01423772 | |
| 655 | 7 | |a Conference papers and proceedings |2 fast | |
| 655 | 7 | |a Conference papers and proceedings |2 lcgft | |
| 655 | 7 | |a L'Aquila (2003) |2 swd | |
| 700 | 1 | |a Geist, Daniel, |d 1961- |0 http://viaf.org/viaf/sourceID/LC|n2003016855 | |
| 700 | 1 | |a Geist, Daniel, |d 1961- |1 http://viaf.org/viaf/85411657 | |
| 700 | 1 | |a Geist, Daniel, |d 1961- | |
| 700 | 1 | |a Tronci, Enrico, |d 1961- |0 http://viaf.org/viaf/sourceID/LC|n2003016856 | |
| 700 | 1 | |a Tronci, Enrico, |d 1961- |1 http://viaf.org/viaf/85412987 | |
| 700 | 1 | |a Tronci, Enrico, |d 1961- | |
| 776 | 1 | |t Informatics (Online) | |
| 830 | 0 | |a Lecture notes in computer science ; |v 2860 | |
| 830 | 0 | |a Lecture notes in computer science |v 2860 |x 0302-9743 |0 http://viaf.org/viaf/sourceID/LC|n42015162 | |
| 830 | 0 | |a Lecture notes in computer science |x 0302-9743 ; |v 2860 | |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 6424925 |s US-CTY |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 4965230 |s US-ICU |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 990092665660203941 |s US-MH |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 003286000 |s US-NCD |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 4993882 |s US-NIC |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 4199214 |s US-NNC |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 9935056153503681 |s US-PU |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 0 | |i 3bec4f87-567f-4c80-a602-db7f2a1685db |l 991038394989706966 |s US-RPB |m correct_hardware_design_and_verification_methods12th_ifip_wg_10_5_adva_____2003_______sprina________________________________________charme_2003________________________p |
| 999 | 1 | 1 | |l 4965230 |s ISIL:US-ICU |t BKS |a ASR-SciASR |b 64272786 |c TK7874.75.C453 2003 |d Library of Congress classification |y 7529268 |p LOANABLE |
| 999 | 1 | 1 | |l 990092665660203941 |s ISIL:US-MH |t BKS |a CAB HD |b AS2S65 |c QA75 .L4 vol. 2860 |d 0 |x 01 BOOK |y 232079466980003941 |p LOANABLE |
| 999 | 1 | 1 | |l 003286000 |s ISIL:US-NCD |t BKS |a LSC PSV |b D02927548. |c 001.64 L471, v. 2860 |d 1 |x BOOK |y 003286000 |p LOANABLE |
| 999 | 1 | 1 | |l 4993882 |s ISIL:US-NIC |t BKS |a engr,anx |b 31924098271160 |c TK7874 .C55 2003 |d lc |k 1 |x Book |y 9c2c6cc1-e948-4917-8b78-5b5b6c2fc063 |p LOANABLE |
| 999 | 1 | 1 | |l 4199214 |s ISIL:US-NNC |t BKS |a off,eng |b CU62926152 |c TK7874.75 .C453 2003 |y 4280193 |p LOANABLE |
| 999 | 1 | 1 | |l 9935056153503681 |s ISIL:US-PU |t BKS |a Libra stor |b 31198037987836 |c TK7874.75 .C453 2003 |d 0 |x BOOK |y 23253217760003681 |p LOANABLE |
| 999 | 1 | 1 | |l 991038394989706966 |s ISIL:US-RPB |t BKS |a ROCK RKSTORAGE |b 31236017030464 |c TK7874.75 .C453 2003 |d 0 |y 23278374950006966 |p LOANABLE |