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

Volume 8, Number 1, February 2006

• Hubert Garavel, John Hatcliff:
  Why you should definitely read this special section. 1-3
  
• Gianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu:
  The saturation algorithm for symbolic state-space exploration. 4-25
  
• Constantinos Bartzis, Tevfik Bultan:
  Efficient BDDs for bounded arithmetic constraints. 26-36
  
• Radu Mateescu:
  CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems. 37-56
  
• Liana Bozga, Yassine Lakhnech, Michaël Périn:
  Pattern-based abstraction for verifying secrecy in protocols. 57-76
  
• Jan Friso Groote, Frank van Ham:
  Interactive visualization of large state spaces. 77-91
  

Volume 8, Number 2, April 2006

• Susanne Graf, Øystein Haugen, Ileana Ober, Bran Selic:
  Preface of "Specification and Validation of Real Time and Embedded systems in UML". 93-96
  
• Jozef Hooman, Mark van der Zwaag:
  A semantics of communicating reactive objects with timing. 97-112
  
• Susanne Graf, Ileana Ober, Iulian Ober:
  A real-time profile for UML. 113-127
  
• Iulian Ober, Susanne Graf, Ileana Ober:
  Validating timed UML models by simulation and verification. 128-145
  
• Robert de Simone, Charles André:
  Towards a "Synchronous Reactive" UML profile? 146-155
  
• Juliana Küster Filipe, Stuart Anderson:
  On a time enriched OCL liveness template. 156-166
  
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska:
  The HybridUML profile for UML 2.0. 167-176
  

Volume 8, Number 3, June 2006

• Kurt Jensen, Andreas Podelski:
  Tools and algorithms for the construction and analysis of systems. 177-179
  
• Antti Valmari:
  What the small Rubik's cube taught me about data structures, information theory, and randomisation. 180-194
  
• Karsten Schmidt:
  Automated generation of a progress measure for the sweep-line method. 195-203
  
• Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek:
  Lower and upper bounds in zone-based abstractions of timed automata. 204-215
  
• Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, David Parker:
  Numerical vs. statistical probabilistic model checking. 216-228
  
• Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman:
  Error explanation with distance metrics. 229-247
  
• Koushik Sen, Grigore Rosu, Gul Agha:
  Online efficient predictive safety analysis of multithreaded programs. 248-260
  
• Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
  Liveness with invisible ranking. 261-279
  
• Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff:
  Checking JML specifications using an extensible software model checking framework. 280-299
  

Volume 8, Numbers 4-5, August 2006

• John S. Fitzgerald, Stefania Gnesi, Dino Mandrioli:
  The industrialization of formal methods. 301-302
  
• Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl:
  Proving the shalls. 303-319
  
• Colin J. Fidge:
  Formal change impact analyses for emulated control software. 321-335
  
• Alan Wassyng, Mark Lawford:
  Software tools for safety-critical software development. 337-354
  

• Enrico Tronci:
  Introductory Paper. 355-358
  
• J. Strother Moore:
  Inductive assertions and operational semantics. 359-371
  
• Hana Chockler, Orna Kupferman, Moshe Y. Vardi:
  Coverage metrics for formal verification. 373-386
  
• Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar:
  Efficient distributed SAT and SAT-based distributed Bounded Model Checking. 387-396
  
• Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli:
  Finite horizon analysis of Markov Chains with the Murphi verifier. 397-409
  
• Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul:
  Putting it all together - Formal verification of the VAMP. 411-430
  
• Kathi Fisler:
  Toward diagrammability and efficiency in event-sequence languages. 431-447
  

• Roberto Bagnara, Patricia M. Hill, Enea Zaffanella:
  Widening operators for powerset domains. 449-466
  

Volume 8, Number 6, November 2006

• Tiziana Margaria, Bernhard Steffen:
  Special Section on "Leveraging Formal Methods". 467-469
  
• Francois Carcenac, Frédéric Boniol:
  A formal framework for verifying distributed embedded systems based on abstraction methods. 471-484
  
• Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue Simonsen, Christian Stefansen:
  Compositional specification of commercial contracts. 485-516
  
• Erwan Jahier, Pascal Raymond, Philippe Baufreton:
  Case studies with Lurette V2. 517-530
  
• Jens Bæk Jørgensen, Søren Christensen, Antti-Pekka Tuovinen, Jianli Xu:
  Tool Support for Estimating the Memory Usage of Mobile Phone Software. 531-545
  
• Yamine Aït Ameur, Mickaël Baron:
  Formal and experimental validation approaches in HCI systems design based on a shared event B model. 547-563
  
• María Alpuente, Demis Ballis, Moreno Falaschi:
  Rule-based verification of Web sites. 565-585
  
• Christopher A. Rouff, Michael G. Hinchey, Walter Truszkowski, James L. Rash:
  Experiences applying formal approaches in the development of swarm-based space exploration systems. 587-603
  

• Peter Buchholz, Joost-Pieter Katoen, Marcel Verhoef:
  Guest editors' introduction: quantitative analysis of real-time embedded systems. 605-606
  
• Joern Ploennigs, Mario Neugebauer, Klaus Kabitzsch:
  Automated model generation for performance engineering of building automation networks. 607-620
  
• Marie Duflot, Marta Z. Kwiatkowska, Gethin Norman, David Parker:
  A formal analysis of bluetooth device discovery. 621-632
  
• Martijn Hendriks, Barend van den Nieuwelaar, Frits W. Vaandrager:
  Model checker aided design of a controller for a wafer scanner. 633-647
  
• Ernesto Wandeler, Lothar Thiele, Marcel Verhoef, Paul Lieverse:
  System architecture evaluation using modular performance analysis: a case study. 649-667