International Journal on Software Tools for Technology Transfer (STTT), Volume 3

Volume 3, Number 1, 2000

• Fausto Giunchiglia, Paolo Traverso:
  Theorem proving in technology transfer: the user's point of view. 1-12
  Electronic Edition (Springer LINK) BibTeX
• Matt Kaufmann:
  Verification of Year 2000 conversion rules using the ACL2 theorem prover. 13-19
  Electronic Edition (Springer LINK) BibTeX
• Ben L. Di Vito:
  High-automation proofs for properties of requirements models. 20-31
  Electronic Edition (Springer LINK) BibTeX
• Deepak Kapur, Mahadevan Subramaniam:
  Using an induction prover for verifying arithmetic circuits. 32-65
  Electronic Edition (Springer LINK) BibTeX
• Serge Autexier, Dieter Hutter, Bruno Langenstein, Heiko Mantel, Georg Rock, Axel Schairer, Werner Stephan, Roland Vogt, Andreas Wolpers:
  VSE: formal methods meet industrial needs. 66-77
  Electronic Edition (Springer LINK) BibTeX
• Paolo Traverso, Piergiorgio Bertoli:
  Mechanized result verification: an industrial application. 78-92
  Electronic Edition (Springer LINK) BibTeX
• Alexander Aiken, Manuel Fähndrich, Zhendong Su:
  Detecting races in Relay Ladder Logic programs. 93-105
  Electronic Edition (Springer LINK) BibTeX

Volume 3, Number 2, 2001

• Ed Brinksma:
  Verification is experimentation! 107-111
  Electronic Edition (Springer LINK) BibTeX

• Rolf Drechsler, Detlef Sieling:
  Binary decision diagrams in theory and practice. 112-136
  Electronic Edition (Springer LINK) BibTeX
• Randal E. Bryant, Yirng-An Chen:
  Verification of arithmetic circuits using binary moment diagrams. 137-155
  Electronic Edition (Springer LINK) BibTeX
• Shin-ichi Minato:
  Zero-suppressed BDDs and their applications. 156-170
  Electronic Edition (Springer LINK) BibTeX
• Fabio Somenzi:
  Efficient manipulation of decision diagrams. 171-181
  Electronic Edition (Springer LINK) BibTeX
• Stefan Höreth:
  A word-level graph manipulation package. 182-192
  Electronic Edition (Springer LINK) BibTeX
• Justin E. Harlow III, Franc Brglez:
  Design of experiments and evaluation of BDD ordering heuristics. 193-206
  Electronic Edition (Springer LINK) BibTeX
• Janett Mohnke, Paul Molitor, Sharad Malik:
  Application of BDDs in Boolean matching techniques for formal logic combinational verification. 207-216
  Electronic Edition (Springer LINK) BibTeX

• Berna L. Massingill, Timothy G. Mattson, Beverly A. Sanders:
  Parallel programming with a pattern language. 217-234
  Electronic Edition (Springer LINK) BibTeX
• Alberto Bartoli, Gianluca Dini, Lanfranco Lopriore:
  Application-controlled memory management in a single address space environment. 235-245
  Electronic Edition (Springer LINK) BibTeX

Volume 3, Number 3, 2001

• Rance Cleaveland:
  Alternative Approaches to Symbolic Verification - Preface by the Section Editor. 247-249
  Electronic Edition (Springer LINK) BibTeX
• Giorgio Delzanno, Andreas Podelski:
  Constraint-based deductive model checking. 250-270
  Electronic Edition (Springer LINK) BibTeX
• Daniel Hirschkoff:
  Bisimulation verification using the up to techniques. 271-285
  Electronic Edition (Springer LINK) BibTeX
• Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet:
  A light-weight framework for hardware verification. 286-313
  Electronic Edition (Springer LINK) BibTeX
• Hubert Garavel, César Viho, Massimo Zendri:
  System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation. 314-331
  Electronic Edition (Springer LINK) BibTeX

• Marieke Huisman, Bart Jacobs, Joachim van den Berg:
  A case study in class library verification: Java's vector class. 332-352
  Electronic Edition (Springer LINK) BibTeX
• Magnus Lindahl, Paul Pettersson, Wang Yi:
  Formal design and analysis of a gear controller. 353-368
  Electronic Edition (Springer LINK) BibTeX

Volume 3, Number 4, 2001

• Kurt Jensen:
  Special Section on the Practical Use of High-Level Petri Nets: Preface by the section editor. 369-371
  Electronic Edition (Springer LINK) BibTeX
• Gérard Berthelot, Laure Petrucci:
  Specification and validation of a concurrent system: an educational project. 372-381
  Electronic Edition (Springer LINK) BibTeX
• Leo Ojala, Nisse Husberg, Teemu Tynjälä:
  Modelling and analysing a distributed dynamic channel allocation algorithm for mobile computing using high-level net methods. 382-393
  Electronic Edition (Springer LINK) BibTeX
• Hartmann J. Genrich, Robert Küffner, Klaus Voss:
  Executable Petri net models for the analysis of metabolic pathways. 394-404
  Electronic Edition (Springer LINK) BibTeX
• Bo Lindstrom:
  Web-based interfaces for simulation of coloured Petri net models. 405-416
  Electronic Edition (Springer LINK) BibTeX
• Simona Bernardi, Susanna Donatelli, András Horváth:
  Implementing compositionality for stochastic Petri nets. 417-430
  Electronic Edition (Springer LINK) BibTeX
• David P. L. Simons, Mariëlle Stoelinga:
  Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. 469-485
  Electronic Edition (Springer LINK) BibTeX

• Matthias Anlauff, Samarjit Chakraborty, Philipp W. Kutter, Alfonso Pierantonio, Lothar Thiele:
  Generating an action notation environment from Montages descriptions. 431-455
  Electronic Edition (Springer LINK) BibTeX
• Alex Aizman:
  Easy concurrency. 456-468
  Electronic Edition (Springer LINK) BibTeX
• Ekkart Kindler, Michael Weber:
  The Petri Net Kernel - An infrastructure for building Petri net tools. 486-497
  Electronic Edition (Springer LINK) BibTeX