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

Volume 8, Number 1, February 2006

Special section on Tools and Algorithms for the Construction and Analysis of Systems

• 
  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

Special Section on Specification and Validation of Models of Real Time and Embedded Systems with UML

• 
  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

Special Section on Tools and Algorithms for the Construction and Analysis of Systems 2004

• 
  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

A View from Formal Methods 2003

• 
  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

Special Section on Recent Advances in Hardware Verification

• 
  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

Special Section on Leveraging Applications of Formal Methods

• 
  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

Special Section on Quantitative Analysis of Real-Time Embedded Systems

• 
  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