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

Volume 3, Number 1, 2000

Theorem Proving

• 
  Fausto Giunchiglia, Paolo Traverso:
  Theorem proving in technology transfer: the user's point of view. 1-12
• 
  Matt Kaufmann:
  Verification of Year 2000 conversion rules using the ACL2 theorem prover. 13-19
• 
  Ben L. Di Vito:
  High-automation proofs for properties of requirements models. 20-31
• 
  Deepak Kapur, Mahadevan Subramaniam:
  Using an induction prover for verifying arithmetic circuits. 32-65
• 
  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
• 
  Paolo Traverso, Piergiorgio Bertoli:
  Mechanized result verification: an industrial application. 78-92
• 
  Alexander Aiken, Manuel Fähndrich, Zhendong Su:
  Detecting races in Relay Ladder Logic programs. 93-105

Volume 3, Number 2, 2001

• 
  Ed Brinksma:
  Verification is experimentation! 107-111

Special Section on BDD

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

Regular Contributions

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

Volume 3, Number 3, 2001

Alternative Approaches to Symbolic Verification

• 
  Rance Cleaveland:
  Alternative Approaches to Symbolic Verification - Preface by the Section Editor. 247-249
• 
  Giorgio Delzanno, Andreas Podelski:
  Constraint-based deductive model checking. 250-270
• 
  Daniel Hirschkoff:
  Bisimulation verification using the up to techniques. 271-285
• 
  Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet:
  A light-weight framework for hardware verification. 286-313
• 
  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

Regular Contributions

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

Volume 3, Number 4, 2001

Special Section on the Practical Use of High-Level Petri Nets

• 
  Kurt Jensen:
  Special Section on the Practical Use of High-Level Petri Nets: Preface by the section editor. 369-371
• 
  Gérard Berthelot, Laure Petrucci:
  Specification and validation of a concurrent system: an educational project. 372-381
• 
  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
• 
  Hartmann J. Genrich, Robert Küffner, Klaus Voss:
  Executable Petri net models for the analysis of metabolic pathways. 394-404
• 
  Bo Lindstrom:
  Web-based interfaces for simulation of coloured Petri net models. 405-416
• 
  Simona Bernardi, Susanna Donatelli, András Horváth:
  Implementing compositionality for stochastic Petri nets. 417-430
• 
  David P. L. Simons, Mariëlle Stoelinga:
  Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. 469-485

Regular Contributions

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