close
1.

電子ブック

EB
edited by Anca Ralescu
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1994  VIII, 136 p.
シリーズ名: Lecture Notes in Artificial Intelligence ; 847
Lecture Notes in Computer Science ; 847
2.

電子ブック

EB
edited by Dieter Hammer
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1989  VI, 243 p.
シリーズ名: Lecture Notes in Computer Science ; 371
目次情報:
3.

電子ブック

EB
edited by Laurence Pierre, Thomas Kropf
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1999  XII, 376 p.
シリーズ名: Lecture Notes in Computer Science ; 1703
目次情報: 続きを見る
Invited Talks
Esterel and Jazz Two Synchronous Languages for Circuit Design / Gérard Berry
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications / Peter Jansen
Proof of Microprocessors
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer / Ravi Hosabettu ; Ganesh Gopalakrishnan ; Mandayam Srivas
Formal Verification of Explicitly Parallel Microprocessors / Byron Cook ; John Launchbury ; John Matthews ; Dick Kieburtz
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic / Miroslav Velev ; Randal Bryant
Model Checking
Model Checking TLA+ Specifications / Yuan Yu ; Panagiotis Manolios ; Leslie Lamport
Efficient Decompositional Model-Checking for Regular Timing Diagrams / Nina Amla ; E. Allen Emerson ; Kedar S. Namjoshi
Vacuity Detection in Temporal Model Checking / Orna Kupferman ; Moshe Vardi
Formal Methods and Industrial Applications
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard / Cindy Eisner
Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors / Y.Xu ; E.Cerny ; A.Silburt ; A.Coady ; Y.Liu ; P.Pownall
Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics / Marius Bozga ; Oded Maler ; Stavros Tripakis
Abstraction and Compositional Techniques From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking / E.Allen Emerson ; Richard J. Trefler
Automatic Error Correction of Large Circuits Using Boolean Decomposi- tion and Abstraction / Dirk W. Hoffmann ; Thomas Kropf
Abstract BDDs: A Technique for Using Abstraction in Model Checking / Edmund Clarke ; Somesh Jha ; Yuan Lu ; Dong Wang
Theorem Proving Related Approaches
Formal Synthesis at the Algorithmic Level / Christian Blumenröhr ; Viktor Sabelfeld
Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving / Mark Aagaard ; Thomas Melham ; John O'Leary
Verification of Infinite State Systems by Compositional Model Checking / K.L.McMillan
Symbolic Simulation/Symbolic Traversal
Formal Verification of Designs with Complex Control by Symbolic Simulation / Gerd Ritter ; Hans Eveking ; Holger Hinrichsen
Hints to Accelerate Symbolic Traversal / Kavita Ravi ; Fabio Somenzi
Specification Languages and Methodologies
Modeling and Checking Networks of Communicating Real-Time Processes / Jürgen Ruf
"Have I Written Enough Properties?" A Method of Comparison between Specification and Implementation / Sagi Katz ; Orna Grumberg ; Danny Geist
Program Slicing of Hardware Description Languages / E.Clarke ; M.Fujita ; S.P.Rajan ; T.Reps ; S.Shankar ; T.Teitelbaum
Posters
Results of the Verification of a Complex Pipelined Machine Model / Jun Sawada ; Warren A. Hunt, Jr
Hazard-Freedom Checking in Speed-Independent Systems / Husnu Yenigun ; Vladimir Levin ; Doron Peled ; Peter Beerel
Yet Another Look at LTL Model Checking / Klaus Schneider
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology / Stefan Hendricx ; Luc Claesen
Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars / George Economakos ; George Papakonstantinou
A Systematic Incrementalization Technique and Its Application to Hardware Design / Steven Johnson ; Yanhong Liu ; Yuchen Zhang
Bisimulation and Model Checking / Kathi Fisler ; Moshe Y. Vardi
Circular Compositional Reasoning about Liveness
Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell / Nancy A. Day ; Jeffrey R. Lewis
Exploiting Retiming in a Guided Simulation Based Validation Methodology / Aarti Gupta ; Pranav Ashar ; Sharad Malik
Fault Models for Embedded Systems / Jens Chr. Godskesen
Validation of Object-Oriented Concurrent Designs by Model Checking / Michaela Huhn ; George Logothetis
Author Index
Invited Talks
Esterel and Jazz Two Synchronous Languages for Circuit Design / Gérard Berry
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications / Peter Jansen
4.

電子ブック

EB
edited by Ganesh Gopalakrishnan, Phillip Windley
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1998  X, 538 p.
シリーズ名: Lecture Notes in Computer Science ; 1522
目次情報: 続きを見る
Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verification / Kenneth L. McMillan
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution / Robert B. Jones ; Jens U. Skakkebaek ; David L. Dill
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking / Miroslav N. Velev ; Randal E. Bryant
Solving Bit-Vector Equations / M.Oliver Moller ; Harald Rueß
The Formal Design of 1M-Gate ASICs / Asgeir Por Eiriksson
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations / Justin E. Harlow III ; Franc Brglez
A Tutorial on Stalmarck's Proof Procedure for Propositional Logic Mary Sheeran and Gunnar Stalmarck
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods / Macha Nikolskaia ; Antoine Rauzy ; David James Sherman
Bisimulation Minimization in an Automata-Theoretic Verification Framework / Kathi Fisler ; Moshe Y. Vardi
Automatic Verification of Mixed-Level Logic Circuits / Keith Hanna
A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk / S. Tasiran ; S.P. Khatri ; S. Yovine ; R.K. Brayton ; A. Sangiovanni-Vincentelli
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints / Fen Jin ; Henrik Hulgaard ; Eduard Cerny
Using MTBDDs for Composition and Model Checking of Real-Time Systems / Jurgen Ruf ; Thomas Kropf
Formal Methods in CAD from an Industrial Perspective / Carl-Johan H. Seger
A Methodology for Automatic Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool / Nazanin Mansouri ; Ranga Vemuri
Combined Formal Post- and Presynthesis Verification in High Level Synthesis / Thomas Lock ; Michael Mendler ; Matthias Mutz
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem / Abdel Mokkedem ; Ravi Hosabettu ; Ganesh Gopalakrishnan
A Performance Study of BDD-Based Model Checking / Bwolen Yang ; David R. O'Hallaron ; Armin Biere ; Olivier Coudert ; Geert Janssen ; Rajeev K. Ranjan ; Fabio Somenzi
Symbolic Model Checking Visualization / Gila Kamhi ; Limor Fix ; Ziv Binyamini
Input Elimination and Abstraction in Model-Checking / Sela Mador-Haim
Symbolic Simulation of the JEM1 Microprocessor / David A. Greve
Symbolic Simulation: An ACL2 Approach / J. Strother Moore
Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study / Amir Pnueli ; T. Arons
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification / Sergey Berezin ; Edmund Clarke ; Yunshan Zhu
Formally Verifying Data and Control with Weak Reachability Invariants / Jeffrey Su
Generalized Reversible Rules / C. Norris Ip
An Assume-Guarantee Rule for Checking Simulation / Thomas A. Henzinger ; Shaz Qadeer ; Sriram K. Rajamani ; Serdar Tasiran
Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared / Sofiene Tahar ; Paul Curzon ; Jianping Lu
An Instruction Set Process Calculus / Shiu-Kai Chin ; Jang Dae Kim
Techniques for Implicit State Enumeration of EFSMs / James H. Kukula ; Tom R. Shiple ; Adnan Aziz
Model Checking on Product Structures / Klaus Schneider
BDDNOW: A Parallel BDD Package / Kim Milvang-Jensen ; Alan J. Hu
Model-Checking VHDL with CV / David Deharbe ; Subash Shankar ; Edmund M. Clarke
Alexandria: A Tool for Hierarchical Verification / Annette Bunker ; Trent N. Larson ; Michael D. Jones ; Phillip J. Windley
PV: An Explicit Enumeration Model-Checker / Ratan Nalumasu
Author Index
Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verification / Kenneth L. McMillan
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution / Robert B. Jones ; Jens U. Skakkebaek ; David L. Dill
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking / Miroslav N. Velev ; Randal E. Bryant
5.

電子ブック

EB
by Donald E. Knuth
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1999  X, 550 p.
シリーズ名: Lecture Notes in Computer Science ; 1750
目次情報: 続きを見る
Readme (a preface)
Contents (a table of contents)
Mmix (a de nition)
Mmix-Arith (a library)
Mmix-Config (a part of MMMIX)
Mmix-Io (a library)
Mmix-Mem (a triviality)
Mmix-Pipe (a part of MMMIX)
Mmix-Sim (a simulator)
Mmixal (an assembler)
Mmmix (a meta-simulator)
Mmotype (a utility program)
Master Index (a table of references)
Readme (a preface)
Contents (a table of contents)
Mmix (a de nition)
6.

電子ブック

EB
edited by George J. Milne, Laurence Pierre
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1993  IX, 275 p.
シリーズ名: Lecture Notes in Computer Science ; 683
目次情報:
7.

電子ブック

EB
edited by Andrzej Hlawiczka, Joao G.S. Silva, Luca Simoncini
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1996  XVI, 444 p.
シリーズ名: Lecture Notes in Computer Science ; 1150
目次情報:
8.

電子ブック

EB
edited by Hermann Hellwagner, Alexander Reinefeld
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1999  XXII, 494 p.
シリーズ名: Lecture Notes in Computer Science ; 1734
目次情報: 続きを見る
SCI and Competitive Interconnects for Cluster Computing / Part I:
The SCI Standard and Applications of SCI / Hermann Hellwagner1:
Introduction / 1.1:
SCI Overview / 1.2:
Background / 1.2.1:
Goals / 1.2.2:
Concepts / 1.2.3:
Discussion / 1.2.4:
The SCI Standard and Some Extensions / 1.3:
Logical Layer / 1.3.1:
Cache Coherence Layer / 1.3.2:
Extensions / 1.3.3:
Applications of SCI / 1.4:
System Area Network for Clusters / 1.4.1:
Memory Interconnect for Cache-Coherent Multiprocessors / 1.4.2:
I/O Subsystem Interconnect / 1.4.3:
Large-Scale Data Acquisition System / 1.4.4:
Related Communication Networks and Concepts / 1.5:
Concluding Remarks / 1.6:
A Comparison of Three Gigabit Technologies: SCI, Myrinet and SGI/Cray T3D / Christian Kurmann ; Thomas Stricker2:
Levels of Comparison / 2.1:
Direct Deposit / 2.2.1:
Message Passing (MPI/PVM) / 2.2.2:
Protocol Emulation (TCP/IP) / 2.2.3:
Gigabit Network Technologies / 2.3:
The Intel 80686 Hardware Platform / 2.3.1:
Myricom Myrinet Technology / 2.3.2:
Dolphin PCI-SCI Technology / 2.3.3:
The SGI/Cray T3D - A Reference Point / 2.3.4:
ATM: QoS - But Still Short of a Gigabit/s / 2.3.5:
Gigabit Ethernet - An Outlook / 2.3.6:
Transfer Modes / 2.4:
Overview / 2.4.1:
"Native" and "Alternate" Transfer Modes in the Three Architectures / 2.4.2:
Performance Evaluation / 2.5:
Performance of Local Memory Copy / 2.5.1:
Performance of Direct Transfers to Remote Memory / 2.5.2:
Performance of MPI/PVM Transfers / 2.5.3:
Performance of TCP/IP Transfers / 2.5.4:
Discussion and Comparison / 2.5.5:
Summary / 2.6:
SCI Hardware / Part II:
Dolphin SCI Adapter Cards / Marius Christian Liaaen ; Hugo Kohmann3:
Overview of the Adapter Cards / 3.1:
Operating Modes of the SCI Cards / 3.3:
SCI Requester / 3.4:
Address Mapping / 3.4.1:
SCI Transaction Handling / 3.4.2:
SCI Packet Requester / 3.4.3:
SCI Responder / 3.5:
Mailbox / 3.5.1:
Access Protection / 3.5.2:
Atomic Access / 3.5.3:
Host Bridge Capabilities / 3.5.4:
DMA Transfers / 3.6:
DMA Transfers on the SBus Card / 3.6.1:
DMA Transfers on the PCI Card / 3.6.2:
Interrupter / 3.7:
Concurrency Issues / 3.8:
Write Assembly / 3.8.1:
Efficient Store Barrier / 3.8.2:
Performance / 3.9:
Applications and Topologies / 3.10:
SAN Interface Adapter / 3.10.1:
Remote I/O Connection and Data Acquisition / 3.10.2:
Switches and Topologies / 3.10.3:
Cluster Software / 3.11:
The TUM PCI/SCI Adapter / Georg Acher ; Wolfgang Karl ; Markus Leberecht4:
The PCI/SCI Adapter Architecture / 4.1:
SCI Packet Encoding and Decoding / 4.3:
Overview of Packet Processing / 4.3.1:
Choosing the Technology / 4.3.2:
Internal Structure of the FPGA / 4.3.3:
Structure of the Packet Manag er as a Microcode Sequencer / 4.3.4:
Microcode Examples / 4.3.5:
Benefits of the Micro Sequencer / 4.3.6:
The SCI Unit / 4.4:
Preliminary Results for the PCI/SCI Adapter / 4.5:
Related Work / 4.6:
Conclusion / 4.7:
Interconnection Networks with SCI / Part III:
Low-Level SCI Protocols and Their Application to Flexible Switches / Andreas C. Döring ; Wolfgang Obelöer ; Gunther Lustig ; Erik Maehle5:
Data Format of SCI Packets / 5.1:
Flow Control / 5.3:
Flow Control in Rings / 5.3.1:
Packet Sequence in SCI / 5.3.2:
Determination of State Transitions / 5.3.3:
Bandwidth Multiplexing / 5.4:
Bandwidth Management in One Ring / 5.4.1:
Idle Symbols / 5.4.2:
Time-Out Determination / 5.4.3:
Network Interface / 5.5:
Requirements / 5.5.1:
Products / 5.5.2:
Routers / 5.6:
Products and Challenges / 5.6.1:
Flexible Router / 5.6.3:
Strip-off Decision / 5.6.4:
Routing Decision and Topology / 5.6.5:
Rule-Based Routing / 5.7:
Conclusion and Outlook / 5.8:
SCI Rings, Switches, and Networks for Data Acquisition Systems / Harald Richter ; Richard Kleber ; Matthias Ohlenroth6:
SCI-based Data Acquisition Systems / 6.1:
SCINET Test Beds / 6.3:
Measurement Results / 6.4:
SCI Switches / 6.5:
Efficient Use of SCI Switches / 6.6:
Multistage SCI Networks / 6.7:
Simulation Results / 6.8:
Summary and Conclusions / 6.9:
Scalability of SCI Ringlets / Geir Horn7:
Do SCI Ringlets Scale in Number of Nodes? / 7.1:
Ringlet Bandwidth Model / 7.2:
Transaction Formats / 7.2.1:
Packet Generation / 7.2.2:
Address Distribution / 7.2.3:
Locality / 7.2.4:
Bypass Rate / 7.2.5:
Echo Packet Rate / 7.2.6:
Output Link Utilization Factor / 7.2.7:
Scalability Evaluation / 7.3:
Common Assumptions / 7.3.1:
Uniform Ringlet Traffic / 7.3.2:
Non-uniform Ringlet Traffic / 7.3.3:
Changing Packet Lengths / 7.3.4:
Affordable Scalability Using Multi-Cubes / HÃ¥kon Bugge ; Knut Omang7.4:
Interconnect Overview / 8.1:
Methodology / 8.3:
Analysis / 8.4:
"Hot-Link" Analysis / 8.4.1:
"Hot-B-Link" Analysis / 8.4.2:
Results / 8.5:
Conclusions / 8.6:
Device Driver Software and Low-Level APIs / Part IV:
Interfacing SCI Device Drivers to Linux / Roger Butenuth ; Hans-Ulrich Heiss9:
Layers of Functionality / 9.1:
Address Spaces / 9.2.1:
Levels of Hardware Abstraction / 9.2.2:
Resource Management / 9.2.3:
Virtual Mapping / 9.2.4:
Robustness / 9.2.5:
Why Linux? / 9.3:
Interfaces of the Driver / 9.4:
Hardware / 9.4.1:
Linux / 9.4.2:
User Processes / 9.4.3:
SCI Drivers on Other Nodes / 9.4.4:
SCI Physical Layer API / Volker Lindenstruth ; David B. Gustavson9.5:
Scope of the Standard / 10.1:
SCI Physical Layer API Architecture and Features / 10.2:
Exception Handling / 10.2.1:
Endianness / 10.2.2:
Supported Data Types / 10.3:
Miscellaneous Procedures / 10.4:
Address Translation Model / 10.5:
Global Object Identifier / 10.5.1:
SCI Global Address Resolution / 10.5.2:
Shared Memory Transactions / 10.6:
Packet Transactions / 10.7:
Block Transactions / 10.8:
Message Passing Transactions / 10.9:
Cache Transactions / 10.10:
Message Passing Libraries / 10.11:
SCI Sockets Library / Josef Weidendorfer11:
Rationale / 11.1:
Features and Design / 11.1.2:
Features / 11.2.1:
Components / 11.2.2:
Communication via the SSLib / 11.2.3:
Connection Setup / 11.2.4:
Handling Special System Calls / 11.2.5:
Other Calls Intercepted and Handled by the SSLib / 11.2.6:
Out of Band Data / 11.2.7:
Implementation Aspects / 11.3:
Communication Among Components / 11.3.1:
SSLib Layers / 11.3.2:
Choice of Most Efficient Communication Mechanism / 11.3.3:
SSLib Implementations / 11.3.4:
Control Transfers / 11.3.5:
Functional Tests and Performance / 11.4:
TCP/IP over SCI under Linux / Hüseyin Taskin11.5:
SCIP Structure / 12.1:
Packet Driver Interface / 12.2.1:
Hardware Address Resolution / 12.2.2:
Other Implementation Issues / 12.2.3:
Configuration / 12.3:
Latency / 12.3.2:
Throughput / 12.3.3:
PVM for SCI Clusters / Markus Fischer ; Alexander Reinefeld12.4:
Parallel Virtual Machine / 13.1:
PVM Implementations / 13.2.1:
Models for Zero-Memory-Copy Data Transfer / 13.2.2:
SCI Communication Model / 13.3:
PVM-SCI / 13.4:
System Architecture / 13.4.1:
Supporting Multiple Interconnects / 13.4.2:
Reducing Memory Copies / 13.4.3:
Ring Buffer Management / 13.4.4:
Performance Results / 13.4.5:
ScaMPI - Design and Implementation / L.P. Huse ; K. Omang ; H. Bugge ; H. Ry ; A.T. Haugsdal ; E. Rustad13.5:
Scali Systems / 14.1:
The SCI Memory Model / 14.3:
Coordinating Use of Shared Locations / 14.3.1:
Ensuring Safe Data Transport in SCI - Checkpointing / 14.3.2:
Shared Address Space Programming without the Drawbacks / 14.3.3:
ScaMPI Design Goals / 14.4:
ScaMPI Implementation / 14.5:
Fault Tolerance / 14.5.1:
User Friendliness / 14.5.2:
Third Party Software / 14.5.3:
Barrier / 14.6:
All-to-All Communication / 14.6.2:
Shared Memory Programming Models and Runtime Mechanisms / 14.7:
Shared Memory vs Message Passing on SCI: A CaseStudy Using Split-C / Max Ibel ; Michael Schmitt ; Klaus Schauser ; Anurag Acharya15:
Introduction to Split-C / 15.1:
Introduction to Active Messages / 15.1.2:
Message-Passing Implementation / 15.2:
Active Messages on Top of SCI / 15.2.1:
Split-C on Top of Active Messages / 15.2.2:
Shared Memory Implementation / 15.3:
Split-C on Top of SCI / 15.3.1:
Experimental Evaluation / 15.4:
Micro-benchmarks / 15.4.1:
SCI and Competitive Interconnects for Cluster Computing / Part I:
The SCI Standard and Applications of SCI / Hermann Hellwagner1:
Introduction / 1.1:
9.

電子ブック

EB
edited by Jose Rolim
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1999  XXXIV, 1444 p. 365 illus.
シリーズ名: Lecture Notes in Computer Science ; 1586
目次情報:
10.

電子ブック

EB
edited by Wayne Luk, Peter Y.K. Cheung, Manfred Glesner
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg, 1997  XII, 512 p.
シリーズ名: Lecture Notes in Computer Science ; 1304
目次情報:
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼